alex-eg
6f54bfbe08
The type IR, unification with the unknown type, constraints and schemes, built and tested on its own. Nothing calls it yet.
310 lines
14 KiB
Scheme
310 lines
14 KiB
Scheme
;;; 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))))))
|