;;; 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))))
      ;; ...and the same the other way round: it is which side is free
      ;; that decides, not which side was written first.
      (let ((r (fresh-rigid-tvar))
            (a (fresh-tvar)))
        (test-assert "rigid first binds the free one" (unify r a #f))
        (test-assert "to the parameter itself" (eq? r (resolve a))))
      (let ((r1 (fresh-rigid-tvar))
            (r2 (fresh-rigid-tvar)))
        (test-error "two parameters do not unify with each other"
                    (unify r1 r2 #f)))))

  (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))))))