restore type inference layer 0
The type IR, unification with the unknown type, constraints and schemes, built and tested on its own. Nothing calls it yet.
This commit is contained in:
9
Makefile
9
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:
|
||||
|
||||
44
infer.module.scm
Normal file
44
infer.module.scm
Normal file
@@ -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")
|
||||
642
infer.scm
Normal file
642
infer.scm
Normal file
@@ -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 <tvar>
|
||||
(%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 <prim>
|
||||
(make-prim name quals)
|
||||
prim-type?
|
||||
(name prim-name)
|
||||
(quals prim-quals))
|
||||
|
||||
(define-record-type <ptr>
|
||||
(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 <array>
|
||||
(make-array-type elt size)
|
||||
array-type?
|
||||
(elt array-elt)
|
||||
(size array-size))
|
||||
|
||||
(define-record-type <fn>
|
||||
(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 <agg>
|
||||
(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 <alias>
|
||||
(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 <unknown>
|
||||
(%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 <type-class>
|
||||
(%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 <scheme>
|
||||
(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))))
|
||||
@@ -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)
|
||||
|
||||
44
tests/infer.module.scm
Normal file
44
tests/infer.module.scm
Normal file
@@ -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")
|
||||
309
tests/infer.scm
Normal file
309
tests/infer.scm
Normal file
@@ -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<?)))
|
||||
|
||||
(test-group "defaulting"
|
||||
(let ((a (fresh-tvar '(numeric))))
|
||||
(default-type-variables! a #f)
|
||||
(test "an open numeric is an int" 'int (unparse-type a)))
|
||||
(let ((a (fresh-tvar '(floating))))
|
||||
(default-type-variables! a #f)
|
||||
(test "an open floating is a double" 'double (unparse-type a)))
|
||||
(let ((a (fresh-tvar)))
|
||||
(test "a variable with nothing known about it cannot be defaulted"
|
||||
#f (default-type-variables! a #f))
|
||||
(test "and stays a hole, for the caller to complain about"
|
||||
'_ (unparse-type a)))
|
||||
;; Defaulting reaches into the structure, since the hole may be
|
||||
;; anywhere: `(var p (* _) ...)'.
|
||||
(let ((t (parse-type '(* _))))
|
||||
(unify (ptr-target t) (fresh-tvar '(numeric)) #f)
|
||||
(default-type-variables! t #f)
|
||||
(test "and it reaches inside a type" '(* int) (unparse-type t))))
|
||||
|
||||
(test-group "user classes"
|
||||
;; A trait bound is the same shape as `numeric', discharged by
|
||||
;; the same procedure -- that is the point of one representation.
|
||||
;; It differs in two rules, and both are stated while there is
|
||||
;; still only one kind of constraint to state them about.
|
||||
(register-class! 'i-ord #f #f #t)
|
||||
(add-struct 'i-circle '(struct i-circle ((r int))))
|
||||
(test "no instance, no entailment" #f (entails? 'i-ord (parse-type '(struct i-circle))))
|
||||
(add-instance! 'i-ord (parse-type '(struct i-circle)))
|
||||
(test "and with one, entailment" #t (entails? 'i-ord (parse-type '(struct i-circle))))
|
||||
;; Instances key on the resolved type, so an alias cannot be
|
||||
;; registered twice under two names.
|
||||
(add-typedef 'i-circle-alias '(typedef i-circle-alias (struct i-circle)))
|
||||
(test "an alias of an instance is the same instance"
|
||||
#t (entails? 'i-ord (parse-type 'i-circle-alias)))
|
||||
;; Decision 2: static dispatch cannot select an instance for a
|
||||
;; type it does not know, so a strict class says no to ? rather
|
||||
;; than shrugging the way `numeric' does.
|
||||
(test "a strict class refuses ?" #f (entails? 'i-ord the-unknown-type))
|
||||
(test "where a lenient one abstains" 'unknown (entails? 'numeric the-unknown-type))
|
||||
;; ...and it has no default to fall back on.
|
||||
(let ((a (fresh-tvar '(i-ord))))
|
||||
(test-error "an unresolved user constraint is an error, not a guess"
|
||||
(default-type-variables! a #f)))))
|
||||
|
||||
(test-group "schemes"
|
||||
;; Nothing generalizes yet. The shape is here because a scheme
|
||||
;; without a constraint list is the wrong shape for every bounded
|
||||
;; generic, and because instantiation is how a generic body gets
|
||||
;; fresh cells instead of a second type for the same one.
|
||||
(let* ((a (fresh-tvar '(numeric)))
|
||||
(id (make-fn-type a (list a) #f))
|
||||
(s (generalize id (list))))
|
||||
(test "the free variable is quantified" 1 (length (scheme-vars s)))
|
||||
(test "carrying its class as the scheme's context"
|
||||
'((numeric)) (list (map car (scheme-constraints s))))
|
||||
|
||||
(let ((one (instantiate s))
|
||||
(two (instantiate s)))
|
||||
(test "an instantiation is still open" '(fn ((_)) _) (unparse-type one))
|
||||
(unify (fn-ret one) (parse-type 'int) #f)
|
||||
(test "solving one instantiation" '(fn ((int)) int) (unparse-type one))
|
||||
(test "leaves the other alone" '(fn ((_)) _) (unparse-type two))
|
||||
(test "and the scheme itself untouched" '(fn ((_)) _) (unparse-type id))))
|
||||
|
||||
(let* ((a (fresh-tvar))
|
||||
(b (fresh-tvar))
|
||||
(s (generalize (make-fn-type a (list b) #f) (list b))))
|
||||
(test "a variable free in the environment is not quantified"
|
||||
1 (length (scheme-vars s)))
|
||||
(let ((inst (instantiate s)))
|
||||
(unify (car (fn-args inst)) (parse-type 'char) #f)
|
||||
(test "so instantiating solves it for everyone" 'char (unparse-type b))))))
|
||||
@@ -10,6 +10,7 @@
|
||||
(include "codegen.scm")
|
||||
(include "args.scm")
|
||||
(include "types.scm")
|
||||
(include "infer.scm")
|
||||
|
||||
;;; Should be the last in the test suite
|
||||
(test-exit)
|
||||
|
||||
@@ -16,6 +16,7 @@
|
||||
stamp-form-source!
|
||||
form-location
|
||||
sex-error
|
||||
sex-warning
|
||||
with-directory
|
||||
)
|
||||
"utils.scm")
|
||||
|
||||
11
utils.scm
11
utils.scm
@@ -138,6 +138,17 @@ wrap a form-building expression."
|
||||
"Signal an error about FORM, prefixed with where it was written."
|
||||
(apply error (string-append (form-location form) message) args))
|
||||
|
||||
(define (sex-warning form message . args)
|
||||
"Report something about FORM that does not stop the compilation.
|
||||
Goes to stderr, prefixed with where the form was written, so a warning
|
||||
reads like an error and sorts alongside one in a build log."
|
||||
(let ((port (current-error-port)))
|
||||
(display (form-location form) port)
|
||||
(display "warning: " port)
|
||||
(display message port)
|
||||
(for-each (lambda (arg) (display " " port) (display arg port)) args)
|
||||
(newline port)))
|
||||
|
||||
(define (stamp-form-source! form src)
|
||||
"Give FORM and every subform that has none the location SRC. Used for
|
||||
macro expansions, which inherit the location of the call site the way a
|
||||
|
||||
Reference in New Issue
Block a user