diff options
Diffstat (limited to 'type')
| -rw-r--r-- | type/README | 1 | ||||
| -rw-r--r-- | type/default.scm | 47 | ||||
| -rw-r--r-- | type/dictionary.scm | 229 | ||||
| -rw-r--r-- | type/expression-typechecking.scm | 364 | ||||
| -rw-r--r-- | type/pattern-binding.scm | 38 | ||||
| -rw-r--r-- | type/type-decl.scm | 337 | ||||
| -rw-r--r-- | type/type-error-handlers.scm | 40 | ||||
| -rw-r--r-- | type/type-macros.scm | 159 | ||||
| -rw-r--r-- | type/type-main.scm | 56 | ||||
| -rw-r--r-- | type/type-vars.scm | 60 | ||||
| -rw-r--r-- | type/type.scm | 32 | ||||
| -rw-r--r-- | type/unify.scm | 154 |
12 files changed, 1517 insertions, 0 deletions
diff --git a/type/README b/type/README new file mode 100644 index 0000000..dc40c55 --- /dev/null +++ b/type/README @@ -0,0 +1 @@ +This directory contains the type inference phase. diff --git a/type/default.scm b/type/default.scm new file mode 100644 index 0000000..529f4f8 --- /dev/null +++ b/type/default.scm @@ -0,0 +1,47 @@ +;;; This handles the default rule. + +(define (maybe-default-ambiguous-tyvar type def module) + (let ((classes (ntyvar-context type))) + (and (not (null? classes)) ; this happens only during cleanup after an error + (let ((non-standard? '#f) + (numeric? '#f)) + (dolist (class classes) + (cond ((eq? (class-kind class) 'numeric) + (setf numeric? '#t)) + ((not (eq? (class-kind class) 'standard)) + (setf non-standard? '#t)))) + (cond ((or non-standard? (not numeric?)) + (remember-context def + (phase-error 'Non-defaultable-ambiguous-context +"An ambiguous context, ~A, cannot be defaulted.~%Ambiguity in call to ~A~%" + classes def)) + '#f) + (else + (find-default-type type classes classes + (tuple-2-2 (assq module *default-decls*))))))))) + +(define (find-default-type tyvar classes all-classes defaults) + (cond ((null? defaults) + (phase-error 'no-default-applies + "Ambiguous context: ~A~%No default applies.~%" + all-classes) + '#f) + ((null? classes) + (instantiate-tyvar tyvar (car defaults)) + '#t) + ((type-in-class? (car defaults) (car classes)) + (find-default-type tyvar (cdr classes) all-classes defaults)) + (else + (find-default-type tyvar all-classes all-classes (cdr defaults))))) + +(define (type-in-class? ntype class) + (let* ((ntype (expand-ntype-synonym ntype)) + (alg (ntycon-tycon ntype)) + (inst (lookup-instance alg class))) + (if (eq? inst '#f) + '#f + (let ((res '#t)) + (do-contexts (c (instance-context inst)) (ty (ntycon-args ntype)) + (when (not (type-in-class? ty c)) + (setf res '#f))) + res)))) diff --git a/type/dictionary.scm b/type/dictionary.scm new file mode 100644 index 0000000..0a0260e --- /dev/null +++ b/type/dictionary.scm @@ -0,0 +1,229 @@ + +;;; type/dictionary.scm + +;;; This function supports dictionary conversion. It creates lambda +;;; variables to bind to the dictionary args needed by the context. +;;; The actual conversion to lambda is done in the cfn. Each tyvar in +;;; the context has an associated mapping from class to dictionary +;;; variable. This mapping depends on the decl containing the placeholder +;;; since different recursive decls share common tyvars. The mapping is +;;; two levels: decl -> class -> var. + +;;; Due to language restrictions this valdef must be a simple variable +;;; definition. + +(define (dictionary-conversion/definition valdef tyvars) + (let* ((var (decl-var valdef)) + (type (var-type var)) + (context (gtype-context type)) + (dict-param-vars '())) + (dolist (c context) + (let ((tyvar (car tyvars)) + (dparams '())) + (when (not (null? c)) + (dolist (class c) + (let ((var (create-temp-var + (string-append "d_" + (symbol->string (def-name class)))))) + (setf (var-force-strict? var) '#t) + (push (tuple class var) dparams) + (push var dict-param-vars))) + (push (tuple valdef dparams) (ntyvar-dict-params tyvar))) + (setf tyvars (cdr tyvars)))) + (setf (valdef-dictionary-args valdef) (nreverse dict-param-vars)))) + +;;; These routines deal with dict-var processing. + +;;; This discharges the tyvars associated with dictionaries. The dict-vars +;;; to be processed at the next level are returned. + +(define (process-placeholders placeholders deferred decls) + (if (null? placeholders) + deferred + (let ((d1 (process-placeholder (car placeholders) deferred decls))) + (process-placeholders (cdr placeholders) d1 decls)))) + +;;; This processes a placeholder. The following cases arise: +;;; a) the variable has already been processed (no placeholders remain) - +;;; ignore it. placeholders may contain duplicates so this is likely. +;;; b) the type variable is from an outer type environment (in ng-list) +;;; and should just be passed up to the next level (added to old-placeholders) +;;; c) the type variable is associated with a dictionary parameter +;;; d) the type variable is instantiated to a type constructor +;;; e) the type variable is ambiguous (none of the above) + +(define (process-placeholder p deferred decls) + (let* ((tyvar (placeholder-tyvar p)) + (type (prune tyvar))) + (cond ((ntycon? type) + (process-instantiated-tyvar + (expand-ntype-synonym type) p deferred decls)) + ((non-generic? type) + (cons p deferred)) + ((not (null? (ntyvar-dict-params type))) + (if (dict-placeholder? p) + (placeholder->dict-param p (ntyvar-dict-params type) decls) + (placeholder->method p (ntyvar-dict-params type) decls)) + deferred) + (else + ;; Since default types are monotypes, no new vars will + ;; be added to old-placeholders + (when (maybe-default-ambiguous-tyvar + type (placeholder-overloaded-var p) + (valdef-module (car (placeholder-enclosing-decls p)))) + (process-placeholder p deferred decls)) + deferred)))) + +;;; The type variable is associated with a dictionary parameter. The only +;;; complication here is that the class needed may not be directly available - +;;; it may need to be obtained from the super classes of the parameter +;;; dictionaries. + +(define (placeholder->dict-param p param-vars decls) + (let ((class (dict-placeholder-class p)) + (edecls (dict-placeholder-enclosing-decls p))) + (setf (placeholder-exp p) + (dict-reference-code class (locate-params param-vars edecls decls))))) + +(define (dict-reference-code class param-vars) + (let ((var (assq class param-vars))) + (if (not (eq? var '#f)) + (**var/def (tuple-2-2 var)) + (search-superclasses class param-vars)))) + +(define (locate-params param-vars enclosing-decls decls) + (if (null? (cdr param-vars)) + (tuple-2-2 (car param-vars)) + (let ((decl (search-enclosing-decls enclosing-decls decls))) + (tuple-2-2 (assq decl param-vars))))) + +;;; This finds the first dictionary containing the needed class in its +;;; super classes and generates a selector to get the needed dictionary. + +(define (search-superclasses class param-vars) + (let ((pclass (tuple-2-1 (car param-vars)))) + (if (memq class (class-super* pclass)) + (**dsel/dict pclass class (**var/def (tuple-2-2 (car param-vars)))) + (search-superclasses class (cdr param-vars))))) + +(define (placeholder->method p param-vars decls) + (let* ((method (method-placeholder-method p)) + (class (method-var-class method)) + (edecls (placeholder-enclosing-decls p)) + (params (locate-params param-vars edecls decls))) + (setf (placeholder-exp p) + (method-reference-code method class params)))) + +(define (method-reference-code m c param-vars) + (let ((pclass (tuple-2-1 (car param-vars)))) + (if (or (eq? c pclass) + (memq c (class-super* pclass))) + (let* ((msel (assq m (class-selectors pclass))) + (mvar (tuple-2-2 msel))) + (**app (**var/def mvar) (**var/def (tuple-2-2 (car param-vars))))) + (method-reference-code m c (cdr param-vars))))) + +;;; This is for tyvars instantiated to a tycon. A reference to the +;;; appropriate dictionary is generated. This reference must be recursively +;;; dictionary converted since dictionaries may need subdictionaries +;;; when referenced. + +(define (process-instantiated-tyvar tycon p deferred decls) + (let* ((alg (ntycon-tycon tycon)) + (edecls (placeholder-enclosing-decls p)) + (var (placeholder-overloaded-var p)) + (class (if (dict-placeholder? p) + (dict-placeholder-class p) + (method-var-class (method-placeholder-method p)))) + (instance (lookup-instance alg class))) + (if (dict-placeholder? p) + (mlet (((code def1) + (generate-dict-ref instance tycon deferred decls edecls var))) + (setf (placeholder-exp p) code) + (setf deferred def1)) + (let ((method (method-placeholder-method p))) + (if (every (function null?) (instance-gcontext instance)) + (let ((mvar (tuple-2-2 + (assq method (instance-methods instance))))) + (setf (placeholder-exp p) (**var/def mvar))) + (mlet (((code def1) + (generate-dict-ref + instance tycon deferred decls edecls var)) + (sel (tuple-2-2 (assq method (class-selectors class))))) + (setf (method-placeholder-exp p) (**app (**var/def sel) code)) + (setf deferred def1))))) + deferred)) + +;;; This generates a reference to a specific dictionary and binds +;;; needed subdictionaries. Since subdictionaries may be part of the outer +;;; type environment new placeholders may be generated for later resolution. + +(define (generate-dict-ref instance type deferred decls edecls var) + (let* ((ctxt (instance-gcontext instance)) + (dict (dict-ref-code instance))) + (do-contexts (class ctxt) (ty (ntycon-args type)) + (let ((ntype (prune ty))) + (cond + ((ntycon? ntype) + (mlet ((ntype (expand-ntype-synonym ntype)) + (alg (ntycon-tycon ntype)) + (instance (lookup-instance alg class)) + ((code dv1) + (generate-dict-ref + instance ntype deferred decls edecls var))) + (setf dict (**app dict code)) + (setf deferred dv1))) + ((non-generic? ntype) + (let ((p (**dict-placeholder + class ntype edecls var))) + (setf dict (**app dict p)) + (push p deferred))) + ((null? (ntyvar-dict-params ntype)) + (let ((ref-code (**dict-placeholder + class ntype edecls var))) + (when (maybe-default-ambiguous-tyvar + ntype var (valdef-module (car edecls))) + (process-placeholder ref-code '() decls)) + (setf dict (**app dict ref-code)))) + (else + (let ((p (locate-params (ntyvar-dict-params ntype) edecls decls))) + (setf dict (**app dict (dict-reference-code class p)))))))) + (values dict deferred))) + +;;; The following routines deal with recursive placeholders. The basic +;;; strategy is to pass the entire context as a parameter with each +;;; recursive call (this could be optimized later to make use of an +;;; internal entry point). The basic complication is that the context +;;; of each function in a letrec may be arranged differently. + +;;; This generates a call inside decl 'from' to the var 'to'. Vmap is an +;;; alist from vars to a list of vars corresponding to the gtyvars of +;;; the decl signature. + +(define (recursive-call-code from to vmap) + (let ((exp (**var/def to)) + (tyvars (tuple-2-2 (assq to vmap))) + (contexts (gtype-context (var-type to)))) + (do-contexts (class contexts) (tyvar tyvars) + (setf exp (**app exp (locate-param-var tyvar class from)))) + exp)) + +(define (locate-param-var tyvar class decl) + (let ((vmap (tuple-2-2 (assq decl (ntyvar-dict-params tyvar))))) + (**var/def (tuple-2-2 (assq class vmap))))) + +;;; This is used to get the code for a specific dictionary reference. + +(define (dict-ref-code instance) + (**var/def (instance-dictionary instance))) + +;;; This is used to locate the correct enclosing decl. + +(define (search-enclosing-decls decl-list decls) + (cond ((null? decl-list) + (error "Lost decl in search-enclosing-decls!")) + ((memq (car decl-list) decls) + (car decl-list)) + (else + (search-enclosing-decls (cdr decl-list) decls)))) + diff --git a/type/expression-typechecking.scm b/type/expression-typechecking.scm new file mode 100644 index 0000000..f4606d1 --- /dev/null +++ b/type/expression-typechecking.scm @@ -0,0 +1,364 @@ +;;; This file contains typecheckers for all expressions except vars and +;;; declarations. + +;;; From valdef-structs: +;;; valdef, single-fun-def are in type-decls + +(define-type-checker guarded-rhs + (type-check guarded-rhs rhs rhs-type + (type-check guarded-rhs guard guard-type + (type-unify guard-type *bool-type* + (type-mismatch/fixed (guarded-rhs-guard object) + "Guards must be of type Bool" guard-type)) + (return-type object rhs-type)))) + +;;; These type checkers deal with patterns. + +(define-type-checker as-pat + (type-check as-pat pattern as-type + (setf (var-type (var-ref-var (as-pat-var object))) as-type) + (return-type object as-type))) + +(define-type-checker irr-pat + (type-check irr-pat pattern pattern-type + (return-type object pattern-type))) + +(define-type-checker var-pat + (fresh-type var-type + (setf (var-type (var-ref-var (var-pat-var object))) var-type) + (return-type object var-type))) + +(define-type-checker wildcard-pat + (fresh-type pat-type + (return-type object pat-type))) + +;;; Constant patterns create a piece of code to actually to the +;;; match: ((==) k), where k is the constant. This code is placed in the +;;; match-fn slot of the const-pat and is used by the cfn. + +(define-type-checker const-pat + (let* ((val (const-pat-value object)) + (match-fn (**app (**var/def (core-symbol "==")) val))) + (setf (const-pat-match-fn object) match-fn) + (type-check const-pat match-fn match-type + (fresh-type res-type + (type-unify match-type (**arrow res-type *bool-type*) #f) + (return-type object res-type))))) + +(define-type-checker plus-pat + (let* ((kp (**int (plus-pat-k object))) + (km (**int (- (plus-pat-k object)))) + (match-fn (**app (**var/def (core-symbol "<=")) kp)) + (bind-fn (**app (**var/def (core-symbol "+")) km))) + (setf (plus-pat-match-fn object) match-fn) + (setf (plus-pat-bind-fn object) bind-fn) + (fresh-type res-type + (setf (ntyvar-context res-type) (list (core-symbol "Integral"))) + (type-check plus-pat match-fn match-type + (type-check plus-pat bind-fn bind-type + (type-check plus-pat pattern pat-type + (type-unify match-type (**arrow pat-type *bool-type*) #f) + (type-unify bind-type (**arrow pat-type pat-type) #f) + (type-unify res-type pat-type #f) + (return-type object res-type))))))) + +(define-type-checker pcon + (type-check/list pcon pats arg-types + (fresh-type res-type + (let ((con-type (instantiate-gtype (con-signature (pcon-con object))))) + (type-unify con-type (**arrow/l-2 arg-types res-type) #f) + (return-type object res-type))))) + +(define-type-checker list-pat + (if (null? (list-pat-pats object)) + (return-type object (instantiate-gtype + (algdata-signature (core-symbol "List")))) + (type-check/unify-list list-pat pats element-type + (type-mismatch/list object + "List elements have different types") + (return-type object (**list-of element-type))))) + +;;; These are in the order defined in exp-structs.scm + +(define-type-checker lambda + (with-new-tyvars + (fresh-monomorphic-types (length (lambda-pats object)) arg-vars + (type-check/list lambda pats arg-types + (unify-list arg-types arg-vars) + (type-check lambda body body-type + (return-type object (**arrow/l-2 arg-vars body-type))))))) + +(define-type-checker let + (type-check/decls let decls + (type-check let body let-type + (return-type object let-type)))) + +(define-type-checker if + (type-check if test-exp test-type + (type-unify test-type *bool-type* + (type-mismatch/fixed object + "The test in an if statement must be of type Bool" + test-type)) + (type-check if then-exp then-type + (type-check if else-exp else-type + (type-unify then-type else-type + (type-mismatch object + "then and else clauses have different types" + then-type else-type)) + (return-type object then-type))))) + +(define-type-checker case + (with-new-tyvars + (let ((case-exp object)) ; needed since object is rebound later + (fresh-monomorphic-type arg-type + (type-check case exp exp-type + (type-unify arg-type exp-type #f) ; just to make it monomorphic + (fresh-type res-type + (dolist (object (case-alts object)) + (recover-type-error ;;; %%% Needs work + (type-check alt pat pat-type + (type-unify pat-type arg-type + (type-mismatch case-exp + "Case patterns type conflict." + pat-type arg-type)) + (type-check/decls alt where-decls + (type-check/unify-list alt rhs-list rhs-type + (type-mismatch/list case-exp + "Guarded expressions must have the same type") + (type-unify rhs-type res-type + (type-mismatch case-exp + "Case expression alternatives must have the same type" + rhs-type res-type))))))) + (return-type case-exp res-type))))))) + +;;; Expressions with signatures are transformed into let expressions +;;; with signatures. + +;;; exp :: type is rewritten as +;;; let temp = exp +;;; temp :: type +;;; in temp + +(define-type-checker exp-sign + (type-rewrite + (let* ((temp-var (create-temp-var "TC")) + (decl (**valdef (**var-pat/def temp-var) '() (exp-sign-exp object))) + (let-exp (**let (list decl) (**var/def temp-var))) + (signature (exp-sign-signature object))) + (setf (var-signature temp-var) + (ast->gtype (signature-context signature) + (signature-type signature))) + let-exp))) + +;;; Rather than complicate the ast structure with a new node for dictSel +;;; we recognize the dictSel primitive as an application and treat it +;;; specially. + +(define-type-checker app + (if (and (var-ref? (app-fn object)) + (eq? (var-ref-var (app-fn object)) (core-symbol "dictSel"))) + (type-check-dict-sel (app-arg object)) + (type-check app fn fn-type + (type-check app arg arg-type + (fresh-type res-type + (fresh-type arg-type-1 + (type-unify fn-type (**arrow arg-type-1 res-type) + (type-mismatch/fixed object + "Attempt to call a non-function" + fn-type)) + (type-unify arg-type-1 arg-type + (type-mismatch object + "Argument type mismatch" arg-type-1 arg-type)) + (return-type object res-type))))))) + +;;; This is a special hack for typing dictionary selection as used in +;;; generic tuple functions. This extracts a dictionary from a TupleDict +;;; object and uses is to resolve the overloading of a designated +;;; expression. The expresion must generate exactly one new context. + +(define (type-check-dict-sel arg) + (when (or (not (app? arg)) + (not (app? (app-fn arg)))) + (dict-sel-error)) + (let* ((exp (app-fn (app-fn arg))) + (dict-var (app-arg (app-fn arg))) + (i (app-arg arg)) + (p (dynamic *placeholders*))) + (mlet (((object exp-type) (dispatch-type-check exp))) + ; check for exactly one new context + (when (or (eq? (dynamic *placeholders*) p) + (not (eq? (cdr (dynamic *placeholders*)) p))) + (dict-sel-error)) + (mlet ((placeholder (car (dynamic *placeholders*))) + (tyvar (placeholder-tyvar placeholder)) + ((dict-var-ast dict-var-type) (dispatch-type-check dict-var)) + ((index-ast index-type) (dispatch-type-check i))) + (setf (ntyvar-context tyvar) '()) ; prevent context from leaking out + (setf (dynamic *placeholders*) p) + (type-unify dict-var-type + (**ntycon (core-symbol "TupleDicts") '()) #f) + (type-unify index-type *int-type* #f) + (cond ((method-placeholder? placeholder) + (dict-sel-error)) ; I am lazy. This means that + ; dictSel must not be passed a method + (else + (setf (placeholder-exp placeholder) + (**app (**var/def (core-symbol "dictSel")) + dict-var-ast index-ast)))) + (return-type object exp-type))))) + +(define (dict-sel-error) + (fatal-error 'dict-sel-error "Bad dictSel usage.")) + +(define-type-checker con-ref + (return-type object (instantiate-gtype (con-signature (con-ref-con object))))) + +(define-type-checker integer-const + (cond ((const-overloaded? object) + (setf (const-overloaded? object) '#f) + (type-rewrite (**fromInteger object))) + (else + (return-type object *Integer-type*)))) + +(define-type-checker float-const + (cond ((const-overloaded? object) + (setf (const-overloaded? object) '#f) + (type-rewrite (**fromRational object))) + (else + (return-type object *Rational-type*)))) + +(define-type-checker char-const + (return-type object *char-type*)) + +(define-type-checker string-const + (return-type object *string-type*)) + +(define-type-checker list-exp + (if (null? (list-exp-exps object)) + (return-type object (instantiate-gtype + (algdata-signature (core-symbol "List")))) + (type-check/unify-list list-exp exps element-type + (type-mismatch/list object + "List elements do not share a common type") + (return-type object (**list-of element-type))))) + +(define-type-checker sequence + (type-rewrite (**enumFrom (sequence-from object)))) + +(define-type-checker sequence-to + (type-rewrite (**enumFromTo (sequence-to-from object) + (sequence-to-to object)))) + +(define-type-checker sequence-then + (type-rewrite (**enumFromThen (sequence-then-from object) + (sequence-then-then object)))) + +(define-type-checker sequence-then-to + (type-rewrite (**enumFromThenTo (sequence-then-to-from object) + (sequence-then-to-then object) + (sequence-then-to-to object)))) + +(define-type-checker list-comp + (with-new-tyvars + (dolist (object (list-comp-quals object)) + (if (is-type? 'qual-generator object) + (fresh-type pat-type + (push pat-type (dynamic *non-generic-tyvars*)) + (type-check qual-generator pat pat-type-1 + (type-unify pat-type pat-type-1 #f) + (type-check qual-generator exp qual-exp-type + (type-unify (**list-of pat-type) qual-exp-type + (type-mismatch/fixed object + "Generator expression is not a list" qual-exp-type))))) + (type-check qual-filter exp filter-type + (type-unify filter-type *bool-type* + (type-mismatch/fixed object + "Filter must have type Bool" filter-type))))) + (type-check list-comp exp exp-type + (return-type object (**list-of exp-type))))) + +(define-type-checker section-l + (type-check section-l op op-type + (type-check section-l exp exp-type + (fresh-type a-type + (fresh-type b-type + (fresh-type c-type + (type-unify op-type (**arrow a-type b-type c-type) + (type-mismatch/fixed object + "Binary function required in section" op-type)) + (type-unify b-type exp-type + (type-mismatch object + "Argument type mismatch" b-type exp-type)) + (return-type object (**arrow a-type c-type)))))))) + +(define-type-checker section-r + (type-check section-r op op-type + (type-check section-r exp exp-type + (fresh-type a-type + (fresh-type b-type + (fresh-type c-type + (type-unify op-type (**arrow a-type b-type c-type) + (type-mismatch/fixed object + "Binary function required" op-type)) + (type-unify exp-type a-type + (type-mismatch object + "Argument type mismatch" a-type exp-type)) + (return-type object (**arrow b-type c-type)))))))) + +(define-type-checker omitted-guard + (return-type object *bool-type*)) + +(define-type-checker con-number + (let ((arg-type (instantiate-gtype + (algdata-signature (con-number-type object))))) + (type-check con-number value arg-type1 + (type-unify arg-type arg-type1 #f) + (return-type object *int-type*)))) + +(define-type-checker sel + (let ((con-type (instantiate-gtype + (con-signature (sel-constructor object))))) + (mlet (((res-type exp-type1) (get-ith-type con-type (sel-slot object)))) + (type-check sel value exp-type + (type-unify exp-type exp-type1 #f) + (return-type object res-type))))) + +(define (get-ith-type type i) + (let ((args (ntycon-args type))) ; must be an arrow + (if (eq? i 0) + (values (car args) (get-ith-type/last (cadr args))) + (get-ith-type (cadr args) (1- i))))) + +(define (get-ith-type/last type) + (if (eq? (ntycon-tycon type) (core-symbol "Arrow")) + (get-ith-type/last (cadr (ntycon-args type))) + type)) + +(define-type-checker is-constructor + (let ((alg-type (instantiate-gtype + (algdata-signature + (con-alg (is-constructor-constructor object)))))) + (type-check is-constructor value arg-type + (type-unify arg-type alg-type #f) + (return-type object *bool-type*)))) + +(define-type-checker cast + (type-check cast exp _ + (fresh-type res + (return-type object res)))) + +;;; This is used for overloaded methods. The theory is to avoid supplying +;;; the context at the class level. This type checks the variable as if it had +;;; the supplied signature. + +(define-type-checker overloaded-var-ref + (let* ((var (overloaded-var-ref-var object)) + (gtype (overloaded-var-ref-sig object)) + (ovar-type (var-type var))) + (when (recursive-type? ovar-type) + (error + "Implementation error: overloaded method found a recursive type")) + (mlet (((ntype new-vars) (instantiate-gtype/newvars gtype)) + (object1 (insert-dict-placeholders + (**var/def var) new-vars object))) + (return-type object1 ntype)))) diff --git a/type/pattern-binding.scm b/type/pattern-binding.scm new file mode 100644 index 0000000..769e155 --- /dev/null +++ b/type/pattern-binding.scm @@ -0,0 +1,38 @@ +;;; This implements the pattern binding rule. + +(define (apply-pattern-binding-rule? decls) + (not + (every (lambda (decl) + (or (function-binding? decl) + (simple-pattern-binding-with-signature? decl))) + decls))) + +(define (function-binding? decl) + (let ((defs (valdef-definitions decl))) + (not (null? (single-fun-def-args (car defs)))))) + +(define (simple-pattern-binding-with-signature? decl) + (let ((lhs (valdef-lhs decl)) + (defs (valdef-definitions decl))) + (and (is-type? 'var-pat lhs) + (null? (single-fun-def-args (car defs))) + (not (eq? (var-signature (var-ref-var (var-pat-var lhs))) '#f))))) + +(define (do-pattern-binding-rule decls necessary-tyvars ng-list) + (setf ng-list (append necessary-tyvars ng-list)) + (find-exported-pattern-bindings decls) + ng-list) + +(define (find-exported-pattern-bindings decls) + (dolist (decl decls) + (dolist (var-ref (collect-pattern-vars (valdef-lhs decl))) + (let ((var (var-ref-var var-ref))) + (when (def-exported? var) + (recoverable-error 'exported-pattern-binding + "Can't export pattern binding of ~A~%" var-ref)) + (when (not (eq? (var-signature var) '#f)) + (recoverable-error 'entire-group-needs-signature + "Variable ~A signature declaration ignored~%" var-ref)))))) + + + diff --git a/type/type-decl.scm b/type/type-decl.scm new file mode 100644 index 0000000..790c0ca --- /dev/null +++ b/type/type-decl.scm @@ -0,0 +1,337 @@ +;;; This deals with declarations (let & letrec). The input is a list of +;;; declarations (valdefs) which may contain recursive-decl-groups, as +;;; introduced in dependency analysis. This function alters the list +;;; of non-generic type variables. Expressions containing declarations +;;; need to rebind the non-generic list around the decls and all expressions +;;; within their scope. + +;;; This returns an updated decl list with recursive decl groups removed. + +(define (type-decls decls) + (cond ((null? decls) + '()) + ((is-type? 'recursive-decl-group (car decls)) + (let ((d (recursive-decl-group-decls (car decls)))) + (type-recursive d) + (append d (type-decls (cdr decls))))) + (else + (type-non-recursive (car decls)) + (cons (car decls) + (type-decls (cdr decls)))))) + +;;; This typechecks a mutually recursive group of declarations (valdefs). +;;; Generate a monomorphic variable for each declaration and unify it with +;;; the lhs of the decl. The variable all-vars collects all variables defined +;;; by the declaration group. Save the values of placeholders and ng-list +;;; before recursing. + +;;; The type of each variable is marked as recursive. + +(define (type-recursive decls) + (let ((old-ng (dynamic *non-generic-tyvars*)) + (old-placeholders (dynamic *placeholders*)) + (all-vars '()) + (new-tyvars '()) + (decls+tyvars '())) + ;; on a type error set all types to `a' and give up. + (setf (dynamic *placeholders*) '()) + (recover-type-error + (lambda (r) + (make-dummy-sigs decls) + (setf (dynamic *dict-placeholders*) old-placeholders) + (funcall r)) + ;; Type the lhs of each decl and then mark each variable bound + ;; in the decl as recursive. + (dolist (d decls) + (fresh-type lhs-type + (push lhs-type (dynamic *non-generic-tyvars*)) + (push lhs-type new-tyvars) + (type-decl-lhs d lhs-type) + (push (tuple d lhs-type) decls+tyvars)) + (dolist (var-ref (collect-pattern-vars (valdef-lhs d))) + (let ((var (var-ref-var var-ref))) + (push var all-vars) + (setf (var-type var) + (make recursive-type (type (var-type var)) + (placeholders '())))))) + +;;; This types the decl right hand sides. Each rhs type is unified with the +;;; tyvar corresponding to the lhs. Before checking the signatures, the +;;; ng-list is restored. + + (dolist (d decls+tyvars) + (let ((rhs-type (type-decl-rhs (tuple-2-1 d))) + (lhs-type (tuple-2-2 d))) + (type-unify lhs-type rhs-type + (type-mismatch (tuple-2-1 d) + "Decl type mismatch" lhs-type rhs-type)))) + (setf (dynamic *non-generic-tyvars*) old-ng) + (let ((sig-contexts (check-user-signatures all-vars))) + +;;; This generalizes the signatures of recursive decls. First, the +;;; context of the declaration group is computed. Any tyvar in the +;;; bodies with a non-empty context must appear in all signatures that +;;; are non-ambiguous. + + (let* ((all-tyvars (collect-tyvars/l new-tyvars)) + (overloaded-tyvars '())) + (dolist (tyvar all-tyvars) + (when (and (ntyvar-context tyvar) (not (non-generic? tyvar))) + (push tyvar overloaded-tyvars))) + (reconcile-sig-contexts overloaded-tyvars sig-contexts) + ;; We should probably also emit a warning about inherently + ;; ambiguous decls. + (when (and overloaded-tyvars + (apply-pattern-binding-rule? decls)) + (setf (dynamic *non-generic-tyvars*) + (do-pattern-binding-rule + decls overloaded-tyvars old-ng)) + (setf overloaded-tyvars '())) + ;; The next step is to compute the signatures of the defined + ;; variables and to define all recursive placeholders. When + ;; there is no context the placeholders become simple var refs. + ;; and the types are simply converted. + (cond ((null? overloaded-tyvars) + (dolist (var all-vars) + (let ((r (var-type var))) + (setf (var-type var) (recursive-type-type (var-type var))) + (dolist (p (recursive-type-placeholders r)) + (setf (recursive-placeholder-exp p) + (**var/def var))) + (generalize-type var)))) + ;; When the declaration has a context things get very hairy. + ;; First, grap the recursive placeholders before generalizing the + ;; types. + (else + ;; Mark the overloaded tyvars as read-only. This prevents + ;; signature unification from changing the set of tyvars + ;; defined in the mapping. + (dolist (tyvar overloaded-tyvars) + (setf (ntyvar-read-only? tyvar) '#t)) + (let ((r-placeholders '())) + (dolist (var all-vars) + (let ((rt (var-type var))) + (dolist (p (recursive-type-placeholders rt)) + (push p r-placeholders)) + (setf (var-type var) (recursive-type-type rt)))) + ;; Now compute a signature for each definition and do dictionary + ;; conversion. The var-map defines the actual parameter associated + ;; with each of the overloaded tyvars. + (let ((var-map (map (lambda (decl) + (tuple (decl-var decl) + (generalize-overloaded-type + decl overloaded-tyvars))) + decls))) + ;; Finally discharge each recursive placeholder. + (dolist (p r-placeholders) + (let ((ref-to (recursive-placeholder-var p)) + (decl-from + (search-enclosing-decls + (recursive-placeholder-enclosing-decls p) + decls))) + (setf (recursive-placeholder-exp p) + (recursive-call-code decl-from ref-to var-map))) + ))))) + (setf (dynamic *placeholders*) + (process-placeholders + (dynamic *placeholders*) old-placeholders decls))))))) + +;;; Non-recursive decls are easier. Save the placeholders, use a fresh type +;;; for the left hand side, check signatures, and generalize. + +(define (type-non-recursive decl) + (remember-context decl + (fresh-type lhs-type + (let ((old-placeholders (dynamic *placeholders*)) + (all-vars (map (lambda (x) (var-ref-var x)) + (collect-pattern-vars (valdef-lhs decl))))) + (setf (dynamic *placeholders*) '()) + (recover-type-error + (lambda (r) + (make-dummy-sigs (list decl)) + (setf (dynamic *placeholders*) old-placeholders) + (funcall r)) + (type-decl-lhs decl lhs-type) + (let ((rhs-type (type-decl-rhs decl))) + (type-unify lhs-type rhs-type + (type-mismatch decl + "Decl type mismatch" lhs-type rhs-type))) + (check-user-signatures all-vars) + (let ((all-tyvars (collect-tyvars lhs-type)) + (overloaded-tyvars '())) + (dolist (tyvar all-tyvars) + (when (ntyvar-context tyvar) + (push tyvar overloaded-tyvars))) + (when (and overloaded-tyvars + (apply-pattern-binding-rule? (list decl))) + (setf (dynamic *non-generic-tyvars*) + (do-pattern-binding-rule + (list decl) overloaded-tyvars (dynamic *non-generic-tyvars*))) + (setf overloaded-tyvars '())) + (if (null? overloaded-tyvars) + (dolist (var all-vars) + (generalize-type var)) + (generalize-overloaded-type decl '())) + (setf (dynamic *placeholders*) + (process-placeholders + (dynamic *placeholders*) old-placeholders (list decl))))))))) + +;;; These functions type check definition components. + +;;; This unifies the type of the lhs pattern with a type variable. + +(define (type-decl-lhs object type) + (dynamic-let ((*enclosing-decls* (cons object (dynamic *enclosing-decls*)))) + (remember-context object + (type-check valdef lhs pat-type + (type-unify type pat-type #f))))) + + +;;; This types the right hand side. The *enclosing-decls* variable is +;;; used to keep track of which decl the type checker is inside. This +;;; is needed for both defaulting (to find which module defaults apply) +;;; and recursive types to keep track of the dictionary parameter variables +;;; for recursive references. + +(define (type-decl-rhs object) + (dynamic-let ((*enclosing-decls* (cons object (dynamic *enclosing-decls*)))) + (remember-context object + (type-check/unify-list valdef definitions res-type + (type-mismatch/list object + "Right hand sides have different types") + res-type)))) + + +;;; This is similar to typing lambda. + +(define-type-checker single-fun-def + (fresh-monomorphic-types (length (single-fun-def-args object)) tyvars + (type-check/list single-fun-def args arg-types + (unify-list tyvars arg-types) + (type-check/decls single-fun-def where-decls + (type-check/unify-list single-fun-def rhs-list rhs-type + (type-mismatch/list object + "Bodies have incompatible types") + (return-type object (**arrow/l-2 arg-types rhs-type))))))) + + +;;; These functions are part of the generalization process. + +;;; This function processes user signature declarations for the set of +;;; variables defined in a declaration. Since unification of one signature +;;; may change the type associated with a previously verified signature, +;;; signature unification is done twice unless only one variable is +;;; involved. The context of the signatures is returned to compare +;;; with the overall context of the declaration group. + +(define (check-user-signatures vars) + (cond ((null? (cdr vars)) + (let* ((var (car vars)) + (sig (var-signature var))) + (if (eq? sig '#f) + '() + (list (tuple var (check-var-signature var sig)))))) + (else + (let ((sigs '())) + (dolist (var vars) + (let ((sig (var-signature var))) + (unless (eq? sig '#f) + (check-var-signature var sig)))) + (dolist (var vars) + (let ((sig (var-signature var))) + (unless (eq? sig '#f) + (push (tuple var (check-var-signature var sig)) sigs)))) + sigs)))) + + +(define (check-var-signature var sig) + (mlet (((sig-type sig-vars) (instantiate-gtype/newvars sig))) + (dolist (tyvar sig-vars) + (setf (ntyvar-read-only? tyvar) '#t)) + (type-unify (remove-recursive-type (var-type var)) sig-type + (signature-mismatch var)) + (dolist (tyvar sig-vars) + (setf (ntyvar-read-only? tyvar) '#f)) + sig-vars)) + +;;; Once the declaration context is computed, it must be compared to the +;;; contexts given by the user. All we need to check is that all tyvars +;;; constrained in the user signatures are also in the decl-context. +;;; All user supplied contexts are correct at this point - we just need +;;; to see if some ambiguous portion of the context exists. + +;;; This error message needs work. We need to present the contexts. + +(define (reconcile-sig-contexts overloaded-tyvars sig-contexts) + (dolist (sig sig-contexts) + (let ((sig-vars (tuple-2-2 sig))) + (dolist (d overloaded-tyvars) + (when (not (memq d sig-vars)) + (type-error +"Declaration signature has insufficiant context in declaration~%~A~%" + (tuple-2-1 sig))))))) + +;;; This is used for noisy type inference + +(define (report-typing var) + (when (memq 'type (dynamic *printers*)) + (let* ((name (symbol->string (def-name var)))) + (when (not (or (string-starts? "sel-" name) + (string-starts? "i-" name) + (string-starts? "default-" name) + (string-starts? "dict-" name))) + (format '#t "~A :: ~A~%" var (var-type var)))))) + +;;; This is used during error recovery. When a type error occurs, all +;;; variables defined in the enclosing declaration are set to type `a' +;;; and typing is resumed. + +(define (make-dummy-sigs decls) + (let ((dummy-type (make gtype (context '(())) + (type (**gtyvar 0))))) + (dolist (d decls) + (dolist (var-ref (collect-pattern-vars (valdef-lhs d))) + (let ((var (var-ref-var var-ref))) + (setf (var-type var) dummy-type)))))) + + +;;; This is used to generalize the variable signatures. If there is +;;; an attached signature, the signature is used. Otherwise the ntype +;;; is converted to a gtype. + +(define (generalize-type var) + (if (eq? (var-signature var) '#f) + (setf (var-type var) (ntype->gtype (var-type var))) + (setf (var-type var) (var-signature var))) + (report-typing var)) + +;;; For overloaded types, it is necessary to map the declaration context +;;; onto the generalized type. User signatures may provide different but +;;; equivilant contexts for different declarations in a decl goup. + +;;; The overloaded-vars argument allows ambiguous contexts. This is not +;;; needed for non-recursive vars since the context cannot be ambiguous. + +(define (generalize-overloaded-type decl overloaded-vars) + (let* ((var (decl-var decl)) + (sig (var-signature var)) + (new-tyvars '())) + (cond ((eq? sig '#f) + (mlet (((gtype tyvars) + (ntype->gtype/env (var-type var) overloaded-vars))) + (setf (var-type var) gtype) + (setf new-tyvars tyvars))) + (else + (mlet (((ntype tyvars) (instantiate-gtype/newvars sig))) + (unify ntype (var-type var)) + (setf (var-type var) sig) + (setf new-tyvars (prune/l tyvars))))) + (report-typing var) + (dictionary-conversion/definition decl new-tyvars) + new-tyvars)) + +(define (remove-recursive-type ty) + (if (recursive-type? ty) + (recursive-type-type ty) + ty)) + diff --git a/type/type-error-handlers.scm b/type/type-error-handlers.scm new file mode 100644 index 0000000..ac7af9c --- /dev/null +++ b/type/type-error-handlers.scm @@ -0,0 +1,40 @@ +;;; This file contains error handlers for the type checker. + +(define (type-error msg . args) + (apply (function phase-error) `(type-error ,msg ,@args)) + (report-non-local-type-error) + (continue-from-type-error)) + +(define (report-non-local-type-error) + (when (pair? (dynamic *type-error-handlers*)) + (funcall (car (dynamic *type-error-handlers*))))) + +(define (continue-from-type-error) + (funcall (car (dynamic *type-error-recovery*)))) + +(define (type-mismatch/fixed object msg type) + (format '#t "While typing ~A:~%~A~%Type: ~A~%" object msg type)) + +(define (type-mismatch object msg type1 type2) + (format '#t "While type checking~%~A~%~A~%Types: ~A~% ~A~%" + object msg type1 type2)) + +(define (type-mismatch/list types object msg) + (format '#t "While typing ~A:~%~A~%Types: ~%" object msg) + (dolist (type types) + (format '#t "~A~%" type))) + +;;; Error handlers + +(define (signature-mismatch var) + (format '#t + "Signature mismatch for ~A~%Inferred type: ~A~%Declared type: ~A~%" + var + (remove-type-wrapper (ntype->gtype (var-type var))) + (var-signature var))) + +(define (remove-type-wrapper ty) + (if (recursive-type? ty) (recursive-type-type ty) ty)) + + +
\ No newline at end of file diff --git a/type/type-macros.scm b/type/type-macros.scm new file mode 100644 index 0000000..c6dc168 --- /dev/null +++ b/type/type-macros.scm @@ -0,0 +1,159 @@ + +;;; This file also contains some random globals for the type checker: + +(define-walker type ast-td-type-walker) + +;;; Some pre-defined types +(define *bool-type* '()) +(define *char-type* '()) +(define *string-type* '()) +(define *int-type* '()) +(define *integer-type* '()) +(define *rational-type* '()) + +;;; These two globals are used throughout the typechecker to avoid +;;; passing lots of stuff in each function call. + +(define *placeholders* '()) +(define *non-generic-tyvars* '()) +(define *enclosing-decls* '()) + +;;; Used by the defaulting mechanism + +(define *default-decls* '()) + +;;; Used in error handling & recovery + +(define *type-error-handlers* '()) +(define *type-error-recovery* '()) + + +;;; This associates a type checker function with an ast type. The variable +;;; `object' is bound to the value being types. + +(define-syntax (define-type-checker ast-type . cont) + `(define-walker-method type ,ast-type (object) + ,@cont)) + +;;; This recursively type checks a structure slot in the current object. +;;; This updates the ast in the slot (since type checking rewrites the ast) +;;; and binds the computed type to a variable. The slot must contain an +;;; expression. + +(define-syntax (type-check struct slot var . cont) + `(mlet ((($$$ast$$$ ,var) + (dispatch-type-check (struct-slot ',struct ',slot object)))) + (setf (struct-slot ',struct ',slot object) $$$ast$$$) + ,@cont)) + +;;; This is used to scope decls. + +(define-syntax (with-new-tyvars . cont) + `(dynamic-let ((*non-generic-tyvars* (dynamic *non-generic-tyvars*))) + ,@cont)) + + +;;; Similar to type-check, the slot must contain a list of decls. +;;; This must be done before any reference to a variable defined in the +;;; decls is typechecked. + +(define-syntax (type-check/decls struct slot . cont) + `(with-new-tyvars + (let (($$$decls$$$ + (type-decls (struct-slot ',struct ',slot object)))) + (setf (struct-slot ',struct ',slot object) $$$decls$$$) + ,@cont))) + +;;; The type checker returns an expression / type pair. This +;;; abstracts the returned value. + +(define-syntax (return-type object type) + `(values ,object ,type)) + +;;; When an ast slot contains a list of expressions, there are two +;;; possibilities: the expressions all share the same type or each has +;;; an independant type. In the first case, a single type (computed +;;; by unifying all types in the list) is bound to a variable. + +(define-syntax (type-check/unify-list struct slot var error-handler . cont) + `(mlet ((($$$ast$$$ $$$types$$$) + (do-type-check/list (struct-slot ',struct ',slot object)))) + (setf (struct-slot ',struct ',slot object) $$$ast$$$) + (with-type-error-handler ,error-handler ($$$types$$$) + (unify-list/single-type $$$types$$$) + (let ((,var (car $$$types$$$))) + ,@cont)))) + +;;; When a list of expressions does not share a common type, the result is +;;; a list of types. + +(define-syntax (type-check/list struct slot var . cont) + `(mlet ((($$$ast$$$ ,var) + (do-type-check/list (struct-slot ',struct ',slot object)))) + (setf (struct-slot ',struct ',slot object) $$$ast$$$) + ,@cont)) + +;;; This creates a fresh tyvar and binds it to a variable. + +(define-syntax (fresh-type var . cont) + `(let ((,var (**ntyvar))) + ,@cont)) + +;;; This drives the unification routine. Two types are unified and the +;;; context is updated. Currently no error handling is implemented to +;;; deal with unification errors. + +(define-syntax (type-unify type1 type2 error-handler) + `(with-type-error-handler ,error-handler () + (unify ,type1 ,type2))) + +;;; This generates a fresh set of monomorphic type variables. + +(define-syntax (fresh-monomorphic-types n vars . cont) + `(with-new-tyvars + (let ((,vars '())) + (dotimes (i ,n) + (let ((tv (**ntyvar))) + (push tv ,vars) + (push tv (dynamic *non-generic-tyvars*)))) + ,@cont))) + +;;; This creates a single monomorphic type variable. + +(define-syntax (fresh-monomorphic-type var . cont) + `(let* ((,var (**ntyvar))) + (with-new-tyvars + (push ,var (dynamic *non-generic-tyvars*)) + ,@cont))) + +;;; This is used to rewrite the current ast as a new ast and then +;;; recursively type check the new ast. The original ast is saved for +;;; error message printouts. + +(define-syntax (type-rewrite ast) + `(mlet (((res-ast type) (dispatch-type-check ,ast)) + (res (**save-old-exp object res-ast))) + (return-type res type))) + +;;; These are the type error handlers + +(define-syntax (recover-type-error error-handler . body) + (let ((temp (gensym)) + (err-fn (gensym))) + `(let/cc ,temp + (let ((,err-fn ,error-handler)) + (dynamic-let ((*type-error-recovery* + (cons (lambda () + (funcall ,err-fn ,temp)) + (dynamic *type-error-recovery*)))) + ,@body))))) + +(define-syntax (with-type-error-handler handler extra-args . body) + (if (eq? handler '#f) + `(begin ,@body) + `(dynamic-let ((*type-error-handlers* + (cons (lambda () + (,(car handler) ,@extra-args ,@(cdr handler))) + (dynamic *type-error-handlers*)))) + ,@body))) + diff --git a/type/type-main.scm b/type/type-main.scm new file mode 100644 index 0000000..c5ffe14 --- /dev/null +++ b/type/type-main.scm @@ -0,0 +1,56 @@ + +;;; This is the main entry point to the type checker. + + +(define (do-haskell-type-check object modules) + (type-init modules) + (when (is-type? 'let object) ; may be void + (dynamic-let ((*non-generic-tyvars* '()) + (*placeholders* '()) + (*enclosing-decls* '())) + (type-check/decls let decls + (setf (dynamic *non-generic-tyvars*) '()) + (process-placeholders (dynamic *placeholders*) '() '())))) + 'done) + +;;; This is the main recursive entry to the type checker. + +(define (dispatch-type-check exp) + (remember-context exp + (call-walker type exp))) + +(define (do-type-check/list exps) + (if (null? exps) + (values '() '()) + (mlet (((obj1 type1) (dispatch-type-check (car exps))) + ((objs types) (do-type-check/list (cdr exps)))) + (values (cons obj1 objs) (cons type1 types))))) + +(define (type-init modules) + ;; Built in types + (setf *char-type* (**ntycon (core-symbol "Char") '())) + (setf *string-type* (**ntycon (core-symbol "List") + (list *char-type*))) + (setf *bool-type* (**ntycon (core-symbol "Bool") '())) + (setf *int-type* (**ntycon (core-symbol "Int") '())) + (setf *integer-type* (**ntycon (core-symbol "Integer") '())) + (setf *rational-type* (**ntycon (core-symbol "Ratio") + (list *integer-type*))) + (setf *default-decls* '()) + (dolist (m modules) + (let ((default-types '())) + (dolist (d (default-decl-types (module-default m))) + (let* ((ty (ast->gtype '() d)) + (ntype (gtype-type ty))) + (cond ((not (null? (gtype-context ty))) + (recoverable-error 'not-monotype + "~A is not a monotype in default decl" ty)) + ((not (type-in-class? ntype (core-symbol "Num"))) + (recoverable-error 'not-Num-class + "~A is not in class Num" ty)) + (else + (push ntype default-types))))) + (push (tuple (module-name m) (reverse default-types)) *default-decls*)))) + +(define (remember-placeholder placeholder) + (push placeholder (dynamic *placeholders*))) diff --git a/type/type-vars.scm b/type/type-vars.scm new file mode 100644 index 0000000..4091ce4 --- /dev/null +++ b/type/type-vars.scm @@ -0,0 +1,60 @@ +;;; This type checks a variable. Possible cases: +;;; a) recursive variables +;;; b) method variables +;;; c) generalized variables +;;; d) other variables + +(define-type-checker var-ref + (let* ((var (var-ref-var object)) + (type (var-type var))) + (cond ((method-var? var) +;;; The context of a method variable always has the carrier class +;;; first. + (mlet (((ntype new-tyvars) (instantiate-gtype/newvars type)) + (carrier-tyvar (car new-tyvars)) + (extra-context (cdr new-tyvars)) + (p (**method-placeholder + var carrier-tyvar (dynamic *enclosing-decls*) object)) + (new-object (insert-dict-placeholders p extra-context object))) + (remember-placeholder p) + (return-type (**save-old-exp object new-object) ntype))) + ((recursive-type? type) + (let ((placeholder (**recursive-placeholder + var (dynamic *enclosing-decls*)))) + (push placeholder (recursive-type-placeholders type)) + (return-type placeholder (recursive-type-type type)))) + ((gtype? type) + (mlet (((ntype new-vars) (instantiate-gtype/newvars type)) + (object1 (insert-dict-placeholders object new-vars object))) + (return-type (if (eq? object1 object) + object + (**save-old-exp object object1)) + ntype))) + (else + (return-type object type))))) + +;;; This takes an expression and a context and returns an updated +;;; expression containing placeholders for the context information +;;; implied by the context. Tyvars in the context are added to dict-vars. + +(define (insert-dict-placeholders object tyvars var) + (cond ((null? tyvars) + object) + ((null? (ntyvar-context (car tyvars))) + (insert-dict-placeholders object (cdr tyvars) var)) + (else + (let ((tyvar (car tyvars))) + (insert-dict-placeholders + (insert-dict-placeholders/tyvar + tyvar (ntyvar-context tyvar) object var) + (cdr tyvars) + var))))) + +(define (insert-dict-placeholders/tyvar tyvar classes object var) + (if (null? classes) + object + (let ((p (**dict-placeholder + (car classes) tyvar (dynamic *enclosing-decls*) var))) + (remember-placeholder p) + (insert-dict-placeholders/tyvar tyvar (cdr classes) + (**app object p) var)))) diff --git a/type/type.scm b/type/type.scm new file mode 100644 index 0000000..8a3a82f --- /dev/null +++ b/type/type.scm @@ -0,0 +1,32 @@ +(define-compilation-unit type + (source-filename "$Y2/type/") + (require ast haskell-utils) + (unit type-macros + (source-filename "type-macros.scm")) + (unit unify + (require type-macros) + (source-filename "unify.scm")) + (unit type-main + (require type-macros) + (source-filename "type-main.scm")) + (unit type-decl + (require type-macros) + (source-filename "type-decl.scm")) + (unit dictionary + (require type-macros) + (source-filename "dictionary.scm")) + (unit default + (require type-macros) + (source-filename "default.scm")) + (unit pattern-binding + (require type-macros) + (source-filename "pattern-binding.scm")) + (unit type-vars + (require type-macros) + (source-filename "type-vars.scm")) + (unit expression-typechecking + (require type-macros) + (source-filename "expression-typechecking.scm")) + (unit type-error-handlers + (require type-macros) + (source-filename "type-error-handlers.scm"))) diff --git a/type/unify.scm b/type/unify.scm new file mode 100644 index 0000000..59248c9 --- /dev/null +++ b/type/unify.scm @@ -0,0 +1,154 @@ + +;;; File: type/unify.scm Author: John + +;;; This is the basic unification algorithm used in type checking. + +;;; Unification failure invokes the current type error handler + +;;; Start by removing instantiated type variables from the type. + +(define (unify type1 type2) + (unify-1 (prune type1) (prune type2))) + +;;; The only real tweak here is the read-only bit on type variables. +;;; The rule is that a RO tyvar can be unified only with a generic +;;; non-RO tyvar which has the same or more general context. + +;;; Aside from this, this is standard unification except that context +;;; propagation is needed when a tyvar with a non-empty context is +;;; instantiated. + +;;; If type2 is a tyvar and type1 is not they are switched. + +(define (unify-1 type1 type2) + (cond ((eq? type1 type2) ;; this catches variable to variable unify + 'OK) + ((ntyvar? type1) + (cond ((occurs-in-type type1 type2) + (type-error "Circular type: cannot unify ~A with ~A" + type1 type2)) + ((ntyvar-read-only? type1) + (cond ((or (not (ntyvar? type2)) (ntyvar-read-only? type2)) + (type-error + "Signature too general: cannot unify ~A with ~A" + type1 type2)) + (else + (unify-1 type2 type1)))) + ((and (ntyvar? type2) + (ntyvar-read-only? type2) + (non-generic? type1)) + (type-error + "Type signature cannot be used: monomorphic type variables present.")) + (else + (instantiate-tyvar type1 type2) + (let ((classes (ntyvar-context type1))) + (if (null? classes) + 'OK + (propagate-contexts/ntype type1 type2 classes)))))) + ((ntyvar? type2) + (unify-1 type2 type1)) + ((eq? (ntycon-tycon type1) (ntycon-tycon type2)) + (unify-list (ntycon-args type1) (ntycon-args type2))) + (else + (let ((etype1 (expand-ntype-synonym type1)) + (etype2 (expand-ntype-synonym type2))) + (if (same-tycon? (ntycon-tycon etype1) (ntycon-tycon etype2)) + (unify-list (ntycon-args etype1) (ntycon-args etype2)) + ;; This error message should probably show both the original + ;; and the expanded types for clarity. + (type-error + "Type conflict: type ~A does not match ~A" + etype1 etype2)))))) + + +(define-integrable (instantiate-tyvar tyvar val) + (setf (ntyvar-value tyvar) val)) + +;;; This is needed since interface files may leave multiple def's +;;; for the same tycon sitting around. + +(define (same-tycon? ty1 ty2) + (or (eq? ty1 ty2) + (and (eq? (def-name ty1) (def-name ty2)) + (eq? (def-module ty1) (def-module ty2))))) + + +;;; unifies two lists of types pairwise. Used for tycon args. + +(define (unify-list args1 args2) + (if (null? args1) + 'OK + (begin (unify-list (cdr args1) (cdr args2)) + (unify (car args1) (car args2))))) + +;;; combines a list of types into a single type. Used in constructs +;;; such as [x,y,z] and case expressions. + +(define (unify-list/single-type types) + (when (not (null? types)) + (let ((type (car types))) + (dolist (type2 (cdr types)) + (unify type type2))))) + +;;; This propagates the context from a just instantiated tyvar to the +;;; instantiated value. If the value is a tycon, instances must be +;;; looked up. If the value is a tyvar, the context is added to that of +;;; other tyvar. + +;;; This is used to back out of the unification on errors. This is a +;;; poor mans trail stack! Without this, error messages get very +;;; obscure. + +(define *instantiated-tyvar* '()) + +(define (propagate-contexts/ntype tyvar type classes) + (dynamic-let ((*instantiated-tyvar* tyvar)) + (propagate-contexts/inner type classes))) + +(define (propagate-contexts/inner type classes) + (let ((type (prune type))) + (if (ntyvar? type) + (if (ntyvar-read-only? type) + (if (context-implies? (ntyvar-context type) classes) + 'OK ; no need for context propagation here + (begin + (setf (ntyvar-value (dynamic *instantiated-tyvar*)) '#f) + (type-error "Signature context is too general"))) + (if (null? (ntyvar-context type)) + (setf (ntyvar-context type) classes) + (setf (ntyvar-context type) + (merge-contexts classes (ntyvar-context type))))) + (propagate-contexts-1 (expand-ntype-synonym type) classes)))) + +;;; The type has now been expanded. This propagates each class constraint +;;; in turn. + +(define (propagate-contexts-1 type classes) + (dolist (class classes) + (propagate-single-class type class))) + +;;; Now we have a single class & data type. Either an instance decl can +;;; be found or a type error should be signalled. Once the instance +;;; decl is found, contexts are propagated to the component types. + +(define (propagate-single-class type class) + (let ((instance (lookup-instance (ntycon-tycon type) class))) + (cond ((eq? instance '#f) + ;; This remove the instantiation which caused the type + ;; error - perhaps stop error propagation & make + ;; error message better. + (setf (ntyvar-value (dynamic *instantiated-tyvar*)) '#f) + (type-error "Type ~A is not in class ~A" type class)) + (else + ;; The instance contains a list of class constraints for + ;; each argument. This loop pairs the argument to the + ;; type constructor with the context required by the instance + ;; decl. + (dolist2 (classes (instance-gcontext instance)) + (arg (ntycon-args type)) + (propagate-contexts/inner arg classes))))) + 'OK) + +;;; The routines which handle contexts (merge-contexts and context-implies?) +;;; are in type-utils. The occurs check is also there. + |