diff --git a/Makefile b/Makefile index 759bb42..648e004 100644 --- a/Makefile +++ b/Makefile @@ -26,7 +26,7 @@ INSTALL_PROGRAM = $(INSTALL) MODULE_FLAGS = -emit-all-import-libraries -module-registration -c # Order matters, since module check correctness on compilation -MODULES = utils types sex-macros reader sex-modules semen sex-fmt-c fmt-c-writer sexc +MODULES = utils types infer sex-macros reader sex-modules semen sex-fmt-c fmt-c-writer sexc OBJ = $(MODULES:%=%.o) DEPSFILE = dependencies.txt @@ -63,6 +63,9 @@ utils.o: utils.module.scm utils.scm types.o: types.module.scm types.scm $(CHICKEN_C) $(CSC_FLAGS) $(MODULE_FLAGS) types.module.scm -o types.o -unit types +infer.o: infer.module.scm infer.scm types.o utils.o + $(CHICKEN_C) $(CSC_FLAGS) $(MODULE_FLAGS) infer.module.scm -o infer.o -unit infer -link types,utils + sex-macros.o: sex-macros.module.scm sex-macros.scm $(CHICKEN_C) $(CSC_FLAGS) $(MODULE_FLAGS) sex-macros.module.scm -o sex-macros.o -unit sex-macros @@ -81,8 +84,8 @@ sex-fmt-c.o: sex-fmt-c.scm fmt-c-writer.o: fmt-c-writer.module.scm fmt-c-writer.scm sex-fmt-c.o utils.o $(CHICKEN_C) $(CSC_FLAGS) $(MODULE_FLAGS) fmt-c-writer.module.scm -o fmt-c-writer.o -unit fmt-c-writer -link sex-fmt-c,utils -sexc.o: sexc.module.scm types.o sexc.scm fmt-c-writer.o sex-macros.o sex-modules.o reader.o semen.o utils.o - $(CHICKEN_C) $(CSC_FLAGS) $(MODULE_FLAGS) sexc.module.scm -o sexc.o -unit sexc -link fmt-c-writer,sex-macros,sex-modules,reader,semen,types,utils +sexc.o: sexc.module.scm infer.o types.o sexc.scm fmt-c-writer.o sex-macros.o sex-modules.o reader.o semen.o utils.o + $(CHICKEN_C) $(CSC_FLAGS) $(MODULE_FLAGS) sexc.module.scm -o sexc.o -unit sexc -link fmt-c-writer,sex-macros,sex-modules,reader,semen,infer,types,utils # Unit testing sex-tests: diff --git a/infer.module.scm b/infer.module.scm new file mode 100644 index 0000000..f53f1f3 --- /dev/null +++ b/infer.module.scm @@ -0,0 +1,44 @@ +(module infer + (;; The IR + tvar? + tvar-id + tvar-classes + tvar-rigid? + fresh-tvar + fresh-rigid-tvar + + prim-type? prim-name prim-quals make-prim + ptr-type? ptr-target ptr-quals make-ptr + array-type? array-elt array-size make-array-type + fn-type? fn-ret fn-args fn-variadic? make-fn-type + agg-type? agg-kind agg-name agg-spelling agg-quals make-agg + alias-type? alias-name alias-expansion alias-quals make-alias + unknown-type? the-unknown-type + + resolve + underlying + type-quals + free-tvars + decay + + ;; The boundary + parse-type + unparse-type + + ;; Constraints + register-class! + add-instance! + entails? + default-tvar! + default-type-variables! + + ;; Unification + unify + + ;; Type schemes + scheme? scheme-vars scheme-constraints scheme-type + make-scheme + generalize + instantiate + substitute) + "infer.scm") diff --git a/infer.scm b/infer.scm new file mode 100644 index 0000000..64b19d5 --- /dev/null +++ b/infer.scm @@ -0,0 +1,642 @@ +;;; Type inference, layer 0: the type representation and unification. +;;; +;;; Nothing in the compiler calls this unit yet. It is the ground floor +;;; of the pass described in Type-inference.org -- built and tested on +;;; its own before a single form is routed through it. +;;; +;;; Two representations meet here. *Surface* types are the forms the +;;; rest of the compiler passes around -- `int', `(* const char)', +;;; `(¤ int 16)', `(fn ((int)) int)'. They are what the reader +;;; produces, what the C writer consumes and what `type-match' compares +;;; with `equal?', and they are hopeless for unification. The *IR* +;;; below is the other one: mutable cells, so that solving a type +;;; variable is a side effect rather than a substitution rebuilt at +;;; every step. +;;; +;;; `parse-type' and `unparse-type' are the boundary between the two, +;;; and they carry the whole compatibility burden: `unparse-type' must +;;; produce the exact spelling `type-match' compares against, or the +;;; reflection macros break by silently falling into their `else' +;;; branch. That is what the round-trip test in tests/infer.scm is for, +;;; and why it is driven by every type spelling that appears in the +;;; repository. + +(import + scheme + (scheme base) + (chicken base) + matchable + srfi-1 + srfi-69 + types + utils) + +;;; --------------------------------------------------------------- +;;; The IR +;;; --------------------------------------------------------------- + +;;; A type variable is a mutable cell. `ref' is #f while unsolved and +;;; the type it stands for once bound -- union-find, with the path +;;; compression done in `resolve'. +;;; +;;; `classes' is the list of type classes the variable must satisfy +;;; (`numeric', and one day `ord'); see "constraints" below. `rigid?' +;;; marks a variable that must not unify with anything but itself -- +;;; unused until a `fn' grows type parameters, and five lines now +;;; against an IR change later. +(define-record-type + (%make-tvar id ref classes rigid?) + tvar? + (id tvar-id) + (ref tvar-ref tvar-ref-set!) + (classes tvar-classes tvar-classes-set!) + (rigid? tvar-rigid?)) + +;;; A primitive or otherwise nominal type. `name' is the list of words +;;; making it up, so `int', `(unsigned int)' and `(long long)' are all +;;; one node, and so is a name we have never parsed a declaration for +;;; (`size-t', `GLuint'). The two cases are told apart by +;;; `c-primitive?', which is what keeps a constraint over an unparsed C +;;; typedef from being an error. +(define-record-type + (make-prim name quals) + prim-type? + (name prim-name) + (quals prim-quals)) + +(define-record-type + (make-ptr target quals) + ptr-type? + (target ptr-target) + (quals ptr-quals)) + +;;; `size' is an integer, or #f for `(¤ int)' -- an array of unwritten +;;; length. +(define-record-type + (make-array-type elt size) + array-type? + (elt array-elt) + (size array-size)) + +(define-record-type + (make-fn-type ret args variadic?) + fn-type? + (ret fn-ret) + (args fn-args) + (variadic? fn-variadic?)) + +;;; struct / union / enum. Nominal: two of them are the same type when +;;; they are the same kind and the same name. `spelling' is the surface +;;; form it was written as, kept verbatim so that an aggregate defined +;;; inline in a type position round-trips unchanged. +(define-record-type + (make-agg kind name spelling quals) + agg-type? + (kind agg-kind) + (name agg-name) + (spelling agg-spelling) + (quals agg-quals)) + +;;; A typedef. Transparent to unification -- it unifies as whatever it +;;; expands to -- and opaque to printing, so a diagnostic and a +;;; generated declaration both say `size-t' rather than `unsigned long'. +(define-record-type + (make-alias name expansion quals) + alias-type? + (name alias-name) + (expansion alias-expansion) + (quals alias-quals)) + +;;; `?'. Sex has full C interop, so `printf', `SDL-CreateWindow' and +;;; `size-t' arrive from headers nobody parsed. Rather than reject +;;; every real program, the lattice gets a top element: `?' is +;;; consistent with every type and constrains nothing. +(define-record-type + (%make-unknown) + unknown-type?) + +(define the-unknown-type (%make-unknown)) + +(define tvar-counter 0) + +(define (fresh-tvar . classes) + (set! tvar-counter (+ tvar-counter 1)) + (%make-tvar tvar-counter #f (if (null? classes) (list) (car classes)) #f)) + +(define (fresh-rigid-tvar . classes) + (set! tvar-counter (+ tvar-counter 1)) + (%make-tvar tvar-counter #f (if (null? classes) (list) (car classes)) #t)) + +;;; Follow a bound variable to what it stands for, compressing the path +;;; on the way out. Every procedure that looks at a type's shape starts +;;; here. +(define (resolve type) + (if (and (tvar? type) (tvar-ref type)) + (let ((target (resolve (tvar-ref type)))) + (tvar-ref-set! type target) + target) + type)) + +;;; ...and through any typedef as well, for the places that care what a +;;; type *is* rather than what it is called. +(define (underlying type) + (let ((t (resolve type))) + (if (alias-type? t) + (underlying (alias-expansion t)) + t))) + +(define (type-quals type) + (cond ((prim-type? type) (prim-quals type)) + ((ptr-type? type) (ptr-quals type)) + ((agg-type? type) (agg-quals type)) + ((alias-type? type) (alias-quals type)) + (else (list)))) + +;;; Array-to-pointer and function-to-function-pointer, for the +;;; positions where C decays: a call argument, an operand of `+', the +;;; subscripted half of `(¤ a i)'. +(define (decay type) + (let ((t (underlying type))) + (cond ((array-type? t) (make-ptr (array-elt t) (list))) + ((fn-type? t) (make-ptr t (list))) + (else (resolve type))))) + +(define (free-tvars type) + (let collect ((t type) (acc (list))) + (let ((t (resolve t))) + (cond ((tvar? t) (if (memq t acc) acc (cons t acc))) + ((ptr-type? t) (collect (ptr-target t) acc)) + ((array-type? t) (collect (array-elt t) acc)) + ((alias-type? t) (collect (alias-expansion t) acc)) + ((fn-type? t) (fold collect (collect (fn-ret t) acc) (fn-args t))) + (else acc))))) + +;;; --------------------------------------------------------------- +;;; Surface -> IR +;;; --------------------------------------------------------------- + +(define +qualifiers+ '(const volatile restrict)) + +(define (qualifier? word) (memq word +qualifiers+)) + +;;; `(const char)' written as `((const char))' is the same type: a +;;; sublist that merely groups. The C writer unwraps these too. +(define (maybe-unwrap type) + (if (and (list? type) (= 1 (length type))) + (car type) + type)) + +(define (parse-type surface) + (cond + ((symbol? surface) (parse-words (list surface) (list) surface)) + ((not (pair? surface)) (sex-error surface "not a type" surface)) + ((eq? (car surface) '¤) (parse-array surface)) + ((eq? (car surface) 'fn) (parse-fn surface)) + ((memq '* surface) (parse-pointer-chain surface)) + (else (parse-words surface (list) surface)))) + +;;; A `*'-free run of words: qualifiers, then whatever they qualify. +;;; `form' is only carried along so a complaint can say where it was +;;; written. +(define (parse-words words quals form) + (cond + ((null? words) (sex-error form "type is nothing but qualifiers" form)) + ((qualifier? (car words)) + (parse-words (cdr words) (cons (car words) quals) form)) + ;; A single sublist left: grouping parens, as in (* (const struct s)) + ((and (null? (cdr words)) (pair? (car words))) + (with-quals (parse-type (car words)) (reverse quals))) + ((memq (car words) '(struct union enum)) (parse-agg words (reverse quals))) + ((eq? (car words) '¤) (parse-array words)) + ((eq? (car words) 'fn) (parse-fn words)) + ((memq '* words) (parse-pointer-chain (append (reverse quals) words))) + (else (parse-name words (reverse quals) form)))) + +;;; A name, one word or several: `int', `size-t', `(unsigned int)'. +(define (parse-name words quals form) + (cond + ((not (every symbol? words)) (sex-error form "malformed type" form)) + ;; The type-level wildcard. It is a fresh variable wherever it + ;; appears, which is what makes partial types -- `(* _)', `(¤ _ 4)' + ;; -- fall out for free rather than needing their own grammar. + ((equal? words '(_)) (fresh-tvar)) + ((and (null? (cdr words)) (get-underlying-type (car words))) + => (lambda (target) + (make-alias (car words) (parse-type target) quals))) + (else (make-prim words quals)))) + +;;; ([pub] struct name), (struct name (fields ...)), (struct (fields ...)) +(define (parse-agg words quals) + (let* ((kind (car words)) + (name (and (pair? (cdr words)) (symbol? (cadr words)) (cadr words)))) + (make-agg kind name words quals))) + +;;; (¤ elt ... size) -- the size is the last element when it is an +;;; integer, and absent otherwise. The element words are unwrapped the +;;; way the C writer unwraps them, so `[int 16]' and `[(int) 16]' are +;;; one type. +(define (parse-array surface) + (let* ((rest (cdr surface)) + (sized? (and (pair? rest) (integer? (last rest)))) + (size (and sized? (last rest))) + (words (if sized? (drop-right rest 1) rest))) + (when (null? words) + (sex-error surface "array type without an element type" surface)) + (make-array-type (parse-type (maybe-unwrap words)) size))) + +;;; (fn ((int) (float)) void). Argument entries are types, not named +;;; parameters -- a `fn' in type position has no room for names. +(define (parse-fn surface) + (match surface + (('fn (? list? arglist) ret) + (let* ((variadic? (and (pair? arglist) (variadic-marker? (last arglist)))) + (entries (if variadic? (drop-right arglist 1) arglist))) + (make-fn-type (parse-type ret) + (map (lambda (entry) (parse-type (maybe-unwrap entry))) + entries) + variadic?))) + (else (sex-error surface "malformed function type" surface)))) + +;;; `...' in an arglist, written bare or wrapped the way every other +;;; entry is. +(define (variadic-marker? entry) + (or (eq? entry '...) (equal? entry '(...)))) + +;;; Pointer chains are written flat and read right to left: the last +;;; `*'-separated run is the pointed-to type, and each run before it +;;; qualifies one level of indirection. `(const * const char)' is a +;;; const pointer to a const char. +(define (parse-pointer-chain words) + (let* ((segments (list-split words '*)) + (base (last segments)) + (levels (reverse (drop-right segments 1)))) + (when (null? base) + (sex-error words "pointer to nothing" words)) + (fold (lambda (level acc) + (unless (every qualifier? level) + (sex-error words "only qualifiers may sit between two `*'" words)) + (make-ptr acc level)) + (parse-words (maybe-unwrap-segment base) (list) words) + levels))) + +(define (maybe-unwrap-segment segment) + (let ((s (maybe-unwrap segment))) + (if (list? s) s (list s)))) + +;;; Re-qualify a parsed type, for the grouping case `(const (struct s))' +;;; where the qualifier is read before the thing it qualifies. +(define (with-quals type quals) + (if (null? quals) + type + (cond ((prim-type? type) (make-prim (prim-name type) + (append quals (prim-quals type)))) + ((ptr-type? type) (make-ptr (ptr-target type) + (append quals (ptr-quals type)))) + ((agg-type? type) (make-agg (agg-kind type) (agg-name type) + (agg-spelling type) + (append quals (agg-quals type)))) + ((alias-type? type) (make-alias (alias-name type) + (alias-expansion type) + (append quals (alias-quals type)))) + (else type)))) + +;;; --------------------------------------------------------------- +;;; IR -> surface +;;; --------------------------------------------------------------- + +;;; Every result here has to be the spelling the rest of the compiler +;;; already writes by hand, since `type-match' compares with `equal?' +;;; and a near miss is silent. +(define (unparse-type type) + (let ((t (resolve type))) + (cond + ((tvar? t) '_) + ((unknown-type? t) '?) + ((alias-type? t) (qualify (alias-quals t) (list (alias-name t)))) + ((prim-type? t) (qualify (prim-quals t) (prim-name t))) + ((agg-type? t) (qualify (agg-quals t) (agg-spelling t))) + ((ptr-type? t) + (append (ptr-quals t) (list '*) (as-words (unparse-type (ptr-target t))))) + ((array-type? t) + (let ((elt (as-words (unparse-type (array-elt t))))) + (append (list '¤) + (if (and (pair? elt) (eq? (car elt) '¤)) (list elt) elt) + (if (array-size t) (list (array-size t)) (list))))) + ((fn-type? t) + (list 'fn + (append (map (lambda (arg) (as-arg (unparse-type arg))) (fn-args t)) + (if (fn-variadic? t) (list '(...)) (list))) + (unparse-type (fn-ret t)))) + (else (error "unparse-type: not a type" t))))) + +;;; A one-word type is written bare, anything longer as a list -- +;;; `int', but `(const int)' and `(struct point)'. +(define (qualify quals words) + (let ((all (append quals words))) + (if (and (null? quals) (= 1 (length all))) + (car all) + all))) + +;;; An argument in a `fn' type is written as a list even when it is one +;;; word -- `((int) (float))' -- so only an atom needs wrapping. +(define (as-arg surface) + (if (pair? surface) surface (list surface))) + +;;; Splice a type into a surrounding word list, the way `(* const char)' +;;; and `[* const char]' splice theirs. An array keeps its parentheses: +;;; `(¤ ¤ char 4)' would read back as something else entirely. +(define (as-words surface) + (cond ((not (pair? surface)) (list surface)) + ((memq (car surface) '(¤ fn)) (list surface)) + (else surface))) + +;;; --------------------------------------------------------------- +;;; Constraints +;;; --------------------------------------------------------------- + +;;; `(numeric a)' is already a type class, so it is written as one from +;;; the start: one representation, one table, one entailment check. A +;;; trait bound `(ord (struct circle))' is the same shape, discharged +;;; the same way, and reported by the same procedure -- which is the +;;; whole reason to build it this way while there is only one kind of +;;; constraint to build. +;;; +;;; `default' is the type an unresolved constraint falls back to, the +;;; way Haskell defaults `Num a' to Integer. `test' is how the built-in +;;; classes say "every arithmetic type" without enumerating twenty +;;; spellings as instances; a user trait has no test and lives entirely +;;; in the instance table. `strict?' marks a class that must not be +;;; guessed at: static dispatch needs a real instance, so `?' fails it. +(define-record-type + (%make-type-class name default test strict?) + type-class? + (name type-class-name) + (default type-class-default) + (test type-class-test) + (strict? type-class-strict?)) + +(define +classes+ (make-hash-table)) +(define +instances+ (make-hash-table)) + +(define (register-class! name default test strict?) + (hash-table-set! +classes+ name (%make-type-class name default test strict?))) + +(define (get-class name) + (or (hash-table-ref/default +classes+ name #f) + (error "no such type class" name))) + +;;; Instances key on the *resolved* type, so `(impl show for size-t)' +;;; and `(impl show for unsigned long)' collide rather than quietly +;;; coexisting as two instances of one C type. +(define (instance-key type) + (unparse-type (underlying type))) + +(define (add-instance! class-name type) + (hash-table-set! +instances+ (cons class-name (instance-key type)) #t)) + +(define (has-instance? class-name type) + (hash-table-exists? +instances+ (cons class-name (instance-key type)))) + +;;; #t, #f, or 'unknown -- and the third answer is the important one. +;;; A C name we never parsed a declaration for might well be numeric; +;;; saying #f there would reject working programs, and saying #t would +;;; invent knowledge. 'unknown means "do not constrain, do not +;;; complain". +(define (entails? class-name type) + (let ((cls (get-class class-name)) + (t (underlying type))) + (cond + ((tvar? t) 'unknown) + ;; `?' is consistent with every type, but it entails nothing: + ;; there is no instance to select and no name to mangle. + ((unknown-type? t) (if (type-class-strict? cls) #f 'unknown)) + ((has-instance? class-name t) #t) + ((type-class-test cls) => (lambda (test) (test t))) + (else #f)))) + +(define +integer-words+ '(char short int long signed unsigned bool _Bool)) +(define +float-words+ '(float double)) +(define +known-words+ (append '(void) +integer-words+ +float-words+)) + +;;; A prim built only out of words we recognise. Anything else is a +;;; name from a header, and we have no opinion about it. +(define (c-primitive? t) + (and (prim-type? t) + (every (lambda (word) (memq word +known-words+)) (prim-name t)))) + +(define (void-type? t) + (and (prim-type? t) (equal? (prim-name t) '(void)))) + +(define (arithmetic-type? t) + (cond ((and (agg-type? t) (eq? (agg-kind t) 'enum)) #t) ; an enum is an integer + ((not (prim-type? t)) #f) + ((not (c-primitive? t)) 'unknown) + ((void-type? t) #f) + (else #t))) + +(define (integral-type? t) + (cond ((and (agg-type? t) (eq? (agg-kind t) 'enum)) #t) + ((not (prim-type? t)) #f) + ((not (c-primitive? t)) 'unknown) + ((void-type? t) #f) + ((any (lambda (word) (memq word +float-words+)) (prim-name t)) #f) + (else #t))) + +(define (floating-type? t) + (cond ((not (prim-type? t)) #f) + ((not (c-primitive? t)) 'unknown) + (else (and (any (lambda (word) (memq word +float-words+)) (prim-name t)) + #t)))) + +(define (scalar-type? t) + (cond ((ptr-type? t) #t) + ((array-type? t) #t) ; decays to one + ((fn-type? t) #t) ; likewise + (else (arithmetic-type? t)))) + +;;; The built-ins. They are ordinary classes, registered the same way a +;;; trait will be -- that is the point. +(register-class! 'numeric 'int arithmetic-type? #f) +(register-class! 'integral 'int integral-type? #f) +(register-class! 'floating 'double floating-type? #f) +(register-class! 'scalar #f scalar-type? #f) + +;;; A constraint that survives to the end of a function is defaulted: +;;; `(numeric a)' with nothing else known is an `int'. A *strict* +;;; class has no default and no business guessing, so an unresolved one +;;; is an error -- the rule is worth stating while there is only one +;;; kind of constraint to state it about. +(define (default-tvar! v form) + (let ((strict (find (lambda (c) (type-class-strict? (get-class c))) + (tvar-classes v)))) + (cond + (strict (sex-error form "unresolved constraint" (list strict (unparse-type v)))) + ((find (lambda (c) (type-class-default (get-class c))) (tvar-classes v)) + => (lambda (c) + (tvar-ref-set! v (parse-type (type-class-default (get-class c)))) + #t)) + (else #f)))) + +;;; Default every variable still open in TYPE. Returns #t when none is +;;; left unsolved, so a caller can tell "inferred" from "give up and +;;; ask for the type in writing". +(define (default-type-variables! type form) + (fold (lambda (v ok) (and (default-tvar! v form) ok)) + #t + (free-tvars type))) + +(define (check-classes classes type form) + (for-each + (lambda (c) + (when (eq? #f (entails? c type)) + (sex-error form "type does not satisfy a constraint" + (list c (unparse-type type))))) + classes)) + +;;; --------------------------------------------------------------- +;;; Unification +;;; --------------------------------------------------------------- + +;;; Consistency in the gradual-typing sense rather than equality: `?' +;;; succeeds against anything and binds nothing, which is what keeps +;;; the pass from rejecting every program that includes a C header. +;;; +;;; FORM is carried only so a failure can say where it was written. +(define (unify t1 t2 form) + (let ((a (resolve t1)) + (b (resolve t2))) + (cond + ((eq? a b) #t) + ((unknown-type? a) #t) + ((unknown-type? b) #t) + ((and (tvar? a) (tvar? b) (tvar-rigid? b) (not (tvar-rigid? a))) + (bind-tvar! a b form)) + ((tvar? a) (bind-tvar! a b form)) + ((tvar? b) (bind-tvar! b a form)) + ;; A typedef unifies as what it stands for. Its name survives in + ;; whichever side is printed later, since neither side is rebuilt. + ((alias-type? a) (unify (alias-expansion a) b form)) + ((alias-type? b) (unify a (alias-expansion b) form)) + ((and (prim-type? a) (prim-type? b)) + (check-quals a b form) + (or (equal? (prim-name a) (prim-name b)) + (type-mismatch a b form))) + ((and (ptr-type? a) (ptr-type? b)) + (check-quals a b form) + (unify (ptr-target a) (ptr-target b) form)) + ((and (array-type? a) (array-type? b)) + ;; One of them may be `(¤ int)': an unwritten length constrains + ;; nothing, the way it does not in C either. + (when (and (array-size a) (array-size b) + (not (= (array-size a) (array-size b)))) + (type-mismatch a b form)) + (unify (array-elt a) (array-elt b) form)) + ((and (fn-type? a) (fn-type? b)) + (unless (and (= (length (fn-args a)) (length (fn-args b))) + (eq? (fn-variadic? a) (fn-variadic? b))) + (type-mismatch a b form)) + (unify (fn-ret a) (fn-ret b) form) + (for-each (lambda (x y) (unify x y form)) (fn-args a) (fn-args b)) + #t) + ((and (agg-type? a) (agg-type? b)) + (check-quals a b form) + (or (and (eq? (agg-kind a) (agg-kind b)) + (if (and (agg-name a) (agg-name b)) + (eq? (agg-name a) (agg-name b)) + (equal? (agg-spelling a) (agg-spelling b)))) + (type-mismatch a b form))) + (else (type-mismatch a b form))))) + +(define (type-mismatch a b form) + (sex-error form "type mismatch: expected" + (unparse-type a) 'got (unparse-type b))) + +;;; Qualifiers are compared, and a mismatch is a warning rather than a +;;; failure: C's const-correctness is not this pass's fight yet, and +;;; making it one would reject programs that compile today. +(define (check-quals a b form) + (let ((qa (type-quals a)) + (qb (type-quals b))) + (unless (lset= eq? qa qb) + (sex-warning form "qualifiers differ between" + (unparse-type a) "and" (unparse-type b))))) + +(define (bind-tvar! v t form) + (cond + ;; Without recursive types this cannot trigger. It is four lines, + ;; and the alternative to having it is a hang. + ((occurs? v t) (sex-error form "recursive type" (unparse-type v))) + ;; A rigid variable is a type *parameter*: inside a generic body it + ;; stands for one specific unknown type and must not be solved. + ((tvar-rigid? v) (type-mismatch v t form)) + (else + (when (tvar? t) + (tvar-classes-set! t (lset-union eq? (tvar-classes t) (tvar-classes v)))) + (tvar-ref-set! v t) + (unless (tvar? t) + (check-classes (tvar-classes v) t form)) + #t))) + +(define (occurs? v type) + (let ((t (resolve type))) + (cond ((eq? v t) #t) + ((ptr-type? t) (occurs? v (ptr-target t))) + ((array-type? t) (occurs? v (array-elt t))) + ((alias-type? t) (occurs? v (alias-expansion t))) + ((fn-type? t) (or (occurs? v (fn-ret t)) + (any (lambda (a) (occurs? v a)) (fn-args t)))) + (else #f)))) + +;;; --------------------------------------------------------------- +;;; Type schemes +;;; --------------------------------------------------------------- + +;;; Nothing generalizes yet -- every `fn' in Sex carries a written +;;; signature and there is no polymorphism to abstract over. These are +;;; here because they are ten lines on top of unification and because +;;; they are exactly what a `fn' with type parameters needs, and +;;; because a scheme without a constraint list is the wrong shape for +;;; every bounded generic. `(forall vars constraints type)' it is, +;;; from the start. +(define-record-type + (make-scheme vars constraints type) + scheme? + (vars scheme-vars) + (constraints scheme-constraints) + (type scheme-type)) + +;;; Quantify over everything free in TYPE that is not also free in the +;;; environment, carrying each variable's class constraints along as +;;; the scheme's context. +(define (generalize type env-tvars) + (let ((vars (lset-difference eq? (free-tvars type) env-tvars))) + (make-scheme vars + (append-map (lambda (v) + (map (lambda (c) (cons c v)) (tvar-classes v))) + vars) + type))) + +(define (instantiate scheme) + (let ((subst (map (lambda (v) (cons v (fresh-tvar (tvar-classes v)))) + (scheme-vars scheme)))) + (substitute (scheme-type scheme) subst))) + +;;; Structural copy with the variables in SUBST replaced. Copying is +;;; how a generic body must be handled anyway -- `form-type' is keyed +;;; by cons cell, one form one type, so an instantiation gets fresh +;;; cells rather than a second type for the same cell. +(define (substitute type subst) + (let ((t (resolve type))) + (cond + ((tvar? t) (let ((hit (assq t subst))) (if hit (cdr hit) t))) + ((ptr-type? t) (make-ptr (substitute (ptr-target t) subst) (ptr-quals t))) + ((array-type? t) (make-array-type (substitute (array-elt t) subst) + (array-size t))) + ((alias-type? t) (make-alias (alias-name t) + (substitute (alias-expansion t) subst) + (alias-quals t))) + ((fn-type? t) (make-fn-type (substitute (fn-ret t) subst) + (map (lambda (a) (substitute a subst)) + (fn-args t)) + (fn-variadic? t))) + (else t)))) diff --git a/tests/Makefile b/tests/Makefile index 7297715..0cc5af4 100644 --- a/tests/Makefile +++ b/tests/Makefile @@ -3,10 +3,10 @@ CHICKEN_C = csc CSC_FLAGS += -K prefix -static MODULE_FLAGS = -emit-all-import-libraries -module-registration -c -MODULES = utils types sex-macros reader sex-modules semen sex-fmt-c fmt-c-writer sexc +MODULES = utils types infer sex-macros reader sex-modules semen sex-fmt-c fmt-c-writer sexc SEX_OBJ = $(MODULES:%=%.o) -TESTS = basic semen reader fmt-c-writer utils line-directives codegen args types +TESTS = basic semen reader fmt-c-writer utils line-directives codegen args types infer TEST_SRCS = $(TESTS:%=%.scm) sex-tests: run.scm $(TEST_SRCS) $(SEX_OBJ) @@ -20,6 +20,9 @@ utils.o: utils.module.scm ../utils.scm types.o: types.module.scm ../types.scm $(CHICKEN_C) $(CSC_FLAGS) $(MODULE_FLAGS) types.module.scm -o types.o -unit types +infer.o: infer.module.scm ../infer.scm types.o utils.o + $(CHICKEN_C) $(CSC_FLAGS) $(MODULE_FLAGS) infer.module.scm -o infer.o -unit infer -link types,utils + sex-macros.o: sex-macros.module.scm ../sex-macros.scm $(CHICKEN_C) $(CSC_FLAGS) $(MODULE_FLAGS) sex-macros.module.scm -o sex-macros.o -unit sex-macros @@ -38,8 +41,8 @@ sex-fmt-c.o: ../sex-fmt-c.scm fmt-c-writer.o: fmt-c-writer.module.scm ../fmt-c-writer.scm sex-fmt-c.o utils.o $(CHICKEN_C) $(CSC_FLAGS) $(MODULE_FLAGS) fmt-c-writer.module.scm -o fmt-c-writer.o -unit fmt-c-writer -link sex-fmt-c,utils -sexc.o: sexc.module.scm types.o ../sexc.scm fmt-c-writer.o sex-macros.o sex-modules.o reader.o semen.o utils.o - $(CHICKEN_C) $(CSC_FLAGS) $(MODULE_FLAGS) sexc.module.scm -o sexc.o -unit sexc -link fmt-c-writer,sex-macros,sex-modules,reader,semen,types,utils +sexc.o: sexc.module.scm infer.o types.o ../sexc.scm fmt-c-writer.o sex-macros.o sex-modules.o reader.o semen.o utils.o + $(CHICKEN_C) $(CSC_FLAGS) $(MODULE_FLAGS) sexc.module.scm -o sexc.o -unit sexc -link fmt-c-writer,sex-macros,sex-modules,reader,semen,infer,types,utils clean: rm -f $(SEX_OBJ) diff --git a/tests/infer.module.scm b/tests/infer.module.scm new file mode 100644 index 0000000..5cf5645 --- /dev/null +++ b/tests/infer.module.scm @@ -0,0 +1,44 @@ +(module infer + (;; The IR + tvar? + tvar-id + tvar-classes + tvar-rigid? + fresh-tvar + fresh-rigid-tvar + + prim-type? prim-name prim-quals make-prim + ptr-type? ptr-target ptr-quals make-ptr + array-type? array-elt array-size make-array-type + fn-type? fn-ret fn-args fn-variadic? make-fn-type + agg-type? agg-kind agg-name agg-spelling agg-quals make-agg + alias-type? alias-name alias-expansion alias-quals make-alias + unknown-type? the-unknown-type + + resolve + underlying + type-quals + free-tvars + decay + + ;; The boundary + parse-type + unparse-type + + ;; Constraints + register-class! + add-instance! + entails? + default-tvar! + default-type-variables! + + ;; Unification + unify + + ;; Type schemes + scheme? scheme-vars scheme-constraints scheme-type + make-scheme + generalize + instantiate + substitute) + "../infer.scm") diff --git a/tests/infer.scm b/tests/infer.scm new file mode 100644 index 0000000..587fe1e --- /dev/null +++ b/tests/infer.scm @@ -0,0 +1,309 @@ +;;; Type inference, layer 0. +;;; +;;; Names registered in the type database are prefixed, since the +;;; database is one table shared by every suite in the linked binary. + +(import infer types (chicken sort)) + +;;; Parse and print a surface type again. Everything in this suite goes +;;; through this pair, which is deliberate: they are the only thing the +;;; rest of the compiler will ever see of the IR. +(define (round-trip surface) + (unparse-type (parse-type surface))) + +(test-group "infer" + + (test-group "round-trip" + ;; Every spelling below appears in example/ or tests/, or is one + ;; the C writer documents in walk-type. `type-match' compares types + ;; with equal?, so a near miss here is not a cosmetic bug -- it is + ;; a reflection macro silently falling into its else branch. + (for-each + (lambda (surface) + (test (conc "round-trips: " surface) surface (round-trip surface))) + '(int + void + char + float + double + size-t + GLfloat + (unsigned int) + (long long) + (const int) + (const char) + (* char) + (* void) + (* const char) + (* * char) + (* const * const char) + (const * const char) + (* FILE) + (* SDL-Window) + (struct point) + (struct list-int) + (union value) + (enum mood) + (const struct list-int) + (* struct list-int) + (* const struct point) + (¤ int 16) + (¤ char 512) + (¤ GLfloat 15) + (¤ float) + (¤ * const char) + (¤ * const struct res 32) + (¤ (¤ const char)) + (fn () void) + (fn ((int)) int) + (fn ((int) (int)) int) + (fn ((* const char)) size-t) + (fn ((* const char) (...)) int) + (fn ((¤ float 4)) void))) + + ;; Grouping parens are not part of the type, so these come back + ;; canonicalised rather than verbatim -- which is the whole reason + ;; unparse-type exists rather than "keep what was written". + (test "a grouped element is the same array" '(¤ int 16) (round-trip '(¤ (int) 16))) + (test "a grouped base is the same pointer" '(* const char) + (round-trip '(* (const char)))) + (test "a grouped aggregate keeps its qualifier" '(const struct point) + (round-trip '(const (struct point)))) + + ;; A typedef is transparent to unification and opaque to printing: + ;; the generated declaration has to say what the programmer said. + (add-typedef 'i-handle '(typedef i-handle int)) + (test "a typedef prints as itself" 'i-handle (round-trip 'i-handle)) + (test "and qualified, as itself" '(const i-handle) (round-trip '(const i-handle))) + (test "and under a pointer" '(* i-handle) (round-trip '(* i-handle)))) + + (test-group "wildcards" + (test "a bare _ is a variable" '_ (round-trip '_)) + (test "and composes under a pointer" '(* _) (round-trip '(* _))) + (test "and inside an array" '(¤ _ 4) (round-trip '(¤ _ 4))) + (test "and in a signature" '(fn ((_)) _) (round-trip '(fn ((_)) _))) + + ;; Each _ is its own variable: solving one must not solve the rest. + (let ((t (parse-type '(fn ((_)) _)))) + (unify (car (fn-args t)) (parse-type 'int) #f) + (test "one hole at a time" '(fn ((int)) _) (unparse-type t)))) + + (test-group "structure" + (test-assert "a pointer is a pointer" (ptr-type? (parse-type '(* char)))) + (test "and knows what it points at" 'char + (unparse-type (ptr-target (parse-type '(* char))))) + (test "quals sit on the level they were written at" '(const) + (ptr-quals (parse-type '(const * char)))) + (test "an unsized array has no size" #f (array-size (parse-type '(¤ int)))) + (test "a sized one does" 16 (array-size (parse-type '(¤ int 16)))) + (test "an aggregate is nominal" 'point (agg-name (parse-type '(struct point)))) + (test-assert "a variadic signature says so" + (fn-variadic? (parse-type '(fn ((* const char) (...)) int)))) + (test-assert "and a plain one does not" + (not (fn-variadic? (parse-type '(fn ((int)) int))))) + + ;; decay: the conversion C performs at a call site, an operand of + ;; `+', or the left half of a subscript. + (test "an array decays to a pointer" '(* int) (unparse-type (decay (parse-type '(¤ int 16))))) + (test "a function decays to a pointer to itself" '(* (fn ((int)) int)) + (unparse-type (decay (parse-type '(fn ((int)) int))))) + (test "anything else is left alone" 'int (unparse-type (decay (parse-type 'int))))) + + (test-group "unification" + (test-assert "a type unifies with itself" + (unify (parse-type 'int) (parse-type 'int) #f)) + (test-error "and not with another one" + (unify (parse-type 'int) (parse-type 'char) #f)) + + (let ((a (fresh-tvar))) + (unify a (parse-type '(* const char)) #f) + (test "a variable takes the shape it is unified with" + '(* const char) (unparse-type a))) + + ;; The point of the exercise: `(var p (* _) (& x))' with x : int. + (let ((p (parse-type '(* _)))) + (unify p (parse-type '(* int)) #f) + (test "a partial type is completed by one step" '(* int) (unparse-type p))) + + (let ((a (fresh-tvar)) + (b (fresh-tvar))) + (unify a b #f) + (unify b (parse-type 'double) #f) + (test "two variables joined then solved" 'double (unparse-type a))) + + (test-error "structure has to match" + (unify (parse-type '(* int)) (parse-type '(* char)) #f)) + (test-error "and arity" + (unify (parse-type '(fn ((int)) int)) + (parse-type '(fn ((int) (int)) int)) #f)) + (test-error "and aggregates are told apart by name" + (unify (parse-type '(struct point)) (parse-type '(struct box)) #f)) + (test-error "and by kind" + (unify (parse-type '(struct point)) (parse-type '(union point)) #f)) + + ;; An unwritten array length constrains nothing, the way it does + ;; not in C either. + (test-assert "an unsized array unifies with a sized one" + (unify (parse-type '(¤ int)) (parse-type '(¤ int 16)) #f)) + (test-error "but two written lengths must agree" + (unify (parse-type '(¤ int 4)) (parse-type '(¤ int 16)) #f)) + + ;; A typedef unifies as whatever it stands for. + (add-typedef 'i-count '(typedef i-count int)) + (test-assert "a typedef unifies with its target" + (unify (parse-type 'i-count) (parse-type 'int) #f)) + (let ((a (fresh-tvar))) + (unify a (parse-type 'i-count) #f) + (test "and keeps its name when it is the one printed" + 'i-count (unparse-type a))) + + (test-group "the unknown type" + (test-assert "? is consistent with anything" + (unify the-unknown-type (parse-type '(struct point)) #f)) + (test-assert "in either order" + (unify (parse-type 'int) the-unknown-type #f)) + ;; ...and binds nothing. Degrading to ? is what keeps an + ;; unparsed C declaration from poisoning everything it touches. + (let ((a (fresh-tvar))) + (unify a the-unknown-type #f) + (test "a variable met with ? stays open" '_ (unparse-type a)))) + + (test-group "occurs check" + ;; Unreachable without recursive types, and the alternative to + ;; having it is not an error but a hang. + (let ((a (fresh-tvar))) + (test-error "a variable may not contain itself" + (unify a (make-ptr a (list)) #f)))) + + (test-group "rigid variables" + (let ((r (fresh-rigid-tvar)) + (a (fresh-tvar))) + (test-error "a type parameter does not unify with a type" + (unify r (parse-type 'int) #f)) + (test-assert "an ordinary variable binds to it instead" + (unify a r #f)) + ;; An unsolved variable resolves to itself. + (test-assert "it is still open" (tvar? (resolve r)))))) + + (test-group "constraints" + (test #t (entails? 'numeric (parse-type 'int))) + (test #t (entails? 'numeric (parse-type '(unsigned long)))) + (test #t (entails? 'integral (parse-type 'char))) + (test #f (entails? 'integral (parse-type 'double))) + (test #t (entails? 'floating (parse-type 'double))) + (test #f (entails? 'floating (parse-type 'int))) + (test #f (entails? 'numeric (parse-type '(* char)))) + (test #t (entails? 'scalar (parse-type '(* char)))) + (test #f (entails? 'numeric (parse-type 'void))) + + (add-enum 'i-mood '(enum i-mood (glad sad))) + (test "an enum is an integer" #t (entails? 'integral (parse-type '(enum i-mood)))) + + ;; The third answer, and the important one. A name from a header + ;; might well be numeric; #f would reject working programs and #t + ;; would invent knowledge. + (test "an unparsed C name is not known either way" + 'unknown (entails? 'numeric (parse-type 'size-t))) + (test "nor is an open variable" 'unknown (entails? 'numeric (fresh-tvar))) + (test "? entails nothing, but says so quietly" + 'unknown (entails? 'numeric the-unknown-type)) + + ;; A typedef is entailed by what it resolves to, so an alias cannot + ;; sneak past a constraint its target would fail. + (add-typedef 'i-len '(typedef i-len int)) + (test "a typedef is judged by its target" #t (entails? 'numeric (parse-type 'i-len))) + + ;; A constrained variable checks its classes at the moment it is + ;; solved, not at the end. + (let ((a (fresh-tvar '(numeric)))) + (test-error "solving to a type that fails the class is an error" + (unify a (parse-type '(* char)) #f))) + (let ((a (fresh-tvar '(numeric)))) + (test-assert "and to one that satisfies it is not" + (unify a (parse-type 'double) #f))) + ;; ...but an unparsed name is not a failure, it is an absence of + ;; knowledge, and must stay silent. + (let ((a (fresh-tvar '(numeric)))) + (test-assert "an unparsed C name does not trip a constraint" + (unify a (parse-type 'GLuint) #f))) + + ;; Joining two variables joins what is known about both. + (let ((a (fresh-tvar '(numeric))) + (b (fresh-tvar '(integral)))) + (unify a b #f) + (test "constraints merge when variables do" + '("integral" "numeric") + (sort (map symbol->string (tvar-classes b)) string