;; infer.sx tests — Algorithm W: literals, vars, lambdas, application, let,
;; if, operators, tuples, lists, let-polymorphism.

(define hk-t (fn (src expected)
  (hk-test (str "infer: " src) (hk-infer-type src) expected)))

;; ─── Literals ────────────────────────────────────────────────────────────────
(hk-t "1"          "Int")
(hk-t "3.14"       "Float")
(hk-t "\"hello\""  "String")
(hk-t "'x'"        "Char")
(hk-t "True"       "Bool")
(hk-t "False"      "Bool")

;; ─── Arithmetic and boolean operators ────────────────────────────────────────
(hk-t "1 + 2"      "Int")
(hk-t "3 * 4"      "Int")
(hk-t "10 - 3"     "Int")
(hk-t "True && False" "Bool")
(hk-t "True || False" "Bool")
(hk-t "not True"   "Bool")
(hk-t "1 == 1"     "Bool")
(hk-t "1 < 2"      "Bool")

;; ─── Lambda ───────────────────────────────────────────────────────────────────
;; \x -> x   (identity)  should get t1 -> t1
(hk-test "infer: identity lambda" (hk-infer-type "\\x -> x") "t1 -> t1")

;; \x -> x + 1 : Int -> Int
(hk-test "infer: lambda add" (hk-infer-type "\\x -> x + 1") "Int -> Int")

;; \x -> not x : Bool -> Bool
(hk-test "infer: lambda not" (hk-infer-type "\\x -> not x") "Bool -> Bool")

;; \x y -> x + y : Int -> Int -> Int
(hk-test "infer: two-arg lambda" (hk-infer-type "\\x -> \\y -> x + y") "Int -> Int -> Int")

;; ─── Application ─────────────────────────────────────────────────────────────
(hk-t "not True"    "Bool")
(hk-t "negate 1"    "Int")

;; ─── If-then-else ─────────────────────────────────────────────────────────────
(hk-t "if True then 1 else 2"     "Int")
(hk-t "if 1 == 2 then True else False" "Bool")

;; ─── Let bindings ─────────────────────────────────────────────────────────────
;; let x = 1 in x + 2
(hk-t "let x = 1 in x + 2" "Int")

;; let f x = x + 1 in f 5
(hk-t "let f x = x + 1 in f 5" "Int")

;; let-polymorphism: let id x = x in id 1
(hk-t "let id x = x in id 1" "Int")

;; ─── Tuples ───────────────────────────────────────────────────────────────────
(hk-t "(1, True)"       "(Int, Bool)")
(hk-t "(1, 2, 3)"       "(Int, Int, Int)")

;; ─── Lists ───────────────────────────────────────────────────────────────────
(hk-t "[1, 2, 3]"    "[Int]")
(hk-t "[True, False]" "[Bool]")

;; ─── Polymorphic list functions ───────────────────────────────────────────────
(hk-t "length [1, 2, 3]"   "Int")
(hk-t "null []"             "Bool")
(hk-t "head [1, 2, 3]"     "Int")

;; ─── hk-expr->brief ──────────────────────────────────────────────────────────
(hk-test "brief var"    (hk-expr->brief (list "var" "x"))           "x")
(hk-test "brief con"    (hk-expr->brief (list "con" "Just"))        "Just")
(hk-test "brief int"    (hk-expr->brief (list "int" 42))            "42")
(hk-test "brief app"    (hk-expr->brief (list "app" (list "var" "f") (list "var" "x"))) "(f x)")
(hk-test "brief op"     (hk-expr->brief (list "op" "+" (list "int" 1) (list "int" 2))) "(1 + 2)")
(hk-test "brief lambda" (hk-expr->brief (list "lambda" (list) (list "var" "x"))) "(\\ ...)")
(hk-test "brief loc"    (hk-expr->brief (list "loc" 3 7 (list "var" "x"))) "x")

;; ─── Type error messages ─────────────────────────────────────────────────────
;; Helper: catch the error and check it contains a substring.
(define hk-str-has? (fn (s sub) (>= (index-of s sub) 0)))

(define hk-te
  (fn (label src sub)
    (hk-test label
      (guard (e (#t (hk-str-has? e sub)))
        (begin (hk-infer-type src) false))
      true)))

;; Unbound variable error includes the variable name.
(hk-te "error unbound name" "foo + 1"    "foo")
(hk-te "error unbound unk"  "unknown"    "unknown")

;; Unification error mentions the conflicting types.
(hk-te "error unify int-bool-1" "1 + True"  "Int")
(hk-te "error unify int-bool-2" "1 + True"  "Bool")

;; ─── Loc node: passes through to inner (position decorates outer context) ────
(define hk-loc-err-msg
  (fn ()
    (guard (e (#t e))
      (begin
        (hk-reset-fresh)
        (hk-w (hk-type-env0) (list "loc" 5 10 (list "var" "mystery")))
        "no-error"))))
(hk-test "loc passes through to var error"
  (hk-str-has? (hk-loc-err-msg) "mystery")
  true)

;; ─── hk-infer-decl ───────────────────────────────────────────────────────────
;; Returns ("ok" name type) | ("err" msg)
(define hk-env0-t (hk-type-env0))

(define prog1 (hk-core "f x = x + 1"))
(define decl1 (first (nth prog1 1)))
(define res1 (hk-infer-decl hk-env0-t decl1))
(hk-test "decl result tag"  (first res1)    "ok")
(hk-test "decl result name" (nth res1 1)    "f")
(hk-test "decl result type" (nth res1 2)    "Int -> Int")

;; Error decl: result is ("err" "in 'g': ...")
(define prog2 (hk-core "g x = x + True"))
(define decl2 (first (nth prog2 1)))
(define res2 (hk-infer-decl hk-env0-t decl2))
(hk-test "decl error tag"    (first res2)                  "err")
(hk-test "decl error has g"  (hk-str-has? (nth res2 1) "g")   true)
(hk-test "decl error has msg" (hk-str-has? (nth res2 1) "unify") true)

;; ─── hk-infer-prog ───────────────────────────────────────────────────────────
;; Returns list of ("ok"/"err" ...) tagged results.
(define prog3 (hk-core "double x = x + x\ntwice f x = f (f x)"))
(define results3 (hk-infer-prog prog3 hk-env0-t))
;; results3 = (("ok" "double" "Int -> Int") ("ok" "twice" "..."))
(hk-test "infer-prog count"  (len results3)               2)
(hk-test "infer-prog double" (nth (nth results3 0) 2)     "Int -> Int")
(hk-test "infer-prog twice"  (nth (nth results3 1) 2)     "(t3 -> t3) -> t3 -> t3")

(hk-t "let id x = x in id 1" "Int")

(hk-t "let id x = x in id True" "Bool")

(hk-t "let id x = x in (id 1, id True)" "(Int, Bool)")

(hk-t "let const x y = x in (const 1 True, const True 1)" "(Int, Bool)")

(hk-t "let f x = x in let g y = f y in (g 1, g True)" "(Int, Bool)")

(hk-t "let twice f x = f (f x) in twice (\x -> x + 1) 5" "Int")

{:fails hk-test-fails :pass hk-test-pass :fail hk-test-fail}