// ============================================================================
// PFCL Type Checker — Integration Tests
// ============================================================================
//
// Tests against real catalog composition patterns. Uses a mock catalog with
// type signatures matching the actual 456-function catalog.

use pfcl_typechecker::*;
use std::collections::HashMap;

// ---------------------------------------------------------------------------
// Mock Catalog
// ---------------------------------------------------------------------------

/// A mock catalog that maps function hashes to type schemes.
/// Populated with signatures matching the real PFCL catalog.
struct MockCatalog {
    entries: HashMap<String, TypeScheme>,
}

impl CatalogTypes for MockCatalog {
    fn type_of(&self, hash: &str) -> Option<TypeScheme> {
        self.entries.get(hash).cloned()
    }
}

impl MockCatalog {
    fn new() -> Self {
        MockCatalog {
            entries: HashMap::new(),
        }
    }

    fn add(&mut self, hash: &str, scheme: TypeScheme) {
        self.entries.insert(hash.to_string(), scheme);
    }

    /// Build a catalog with the standard PFCL function signatures.
    fn standard() -> Self {
        let mut cat = MockCatalog::new();

        // Type variable conventions: 0=a, 1=b, 2=c, ...
        let a = TypeVar(100);
        let b = TypeVar(101);
        let c = TypeVar(102);

        // ----- Arithmetic (Layer 1) -----
        // int.add : (Int, Int) → Int
        cat.add(
            "hash:int.add",
            TypeScheme::mono(Type::fun(vec![Type::int(), Type::int()], Type::int())),
        );
        // int.subtract : (Int, Int) → Int
        cat.add(
            "hash:int.subtract",
            TypeScheme::mono(Type::fun(vec![Type::int(), Type::int()], Type::int())),
        );
        // int.multiply : (Int, Int) → Int
        cat.add(
            "hash:int.multiply",
            TypeScheme::mono(Type::fun(vec![Type::int(), Type::int()], Type::int())),
        );
        // int.to_float : Int → Float
        cat.add(
            "hash:int.to_float",
            TypeScheme::mono(Type::fun1(Type::int(), Type::float())),
        );
        // float.divide : (Float, Float) → Float
        cat.add(
            "hash:float.divide",
            TypeScheme::mono(Type::fun(vec![Type::float(), Type::float()], Type::float())),
        );
        // int.greater_than : (Int, Int) → Boolean
        cat.add(
            "hash:int.greater_than",
            TypeScheme::mono(Type::fun(vec![Type::int(), Type::int()], Type::boolean())),
        );
        // int.gt : (Int, Int) → Boolean (alias)
        cat.add(
            "hash:int.gt",
            TypeScheme::mono(Type::fun(vec![Type::int(), Type::int()], Type::boolean())),
        );

        // ----- Comparison (Layer 1) -----
        // equal : (a, a) → Boolean
        cat.add(
            "hash:equal",
            TypeScheme {
                vars: vec![a],
                ty: Type::fun(vec![Type::Var(a), Type::Var(a)], Type::boolean()),
            },
        );

        // ----- Boolean (Layer 1) -----
        // bool.and : (Boolean, Boolean) → Boolean
        cat.add(
            "hash:bool.and",
            TypeScheme::mono(Type::fun(
                vec![Type::boolean(), Type::boolean()],
                Type::boolean(),
            )),
        );
        // bool.not : Boolean → Boolean
        cat.add(
            "hash:bool.not",
            TypeScheme::mono(Type::fun1(Type::boolean(), Type::boolean())),
        );
        // conditional : (Boolean, a, a) → a
        cat.add(
            "hash:conditional",
            TypeScheme {
                vars: vec![a],
                ty: Type::fun(
                    vec![Type::boolean(), Type::Var(a), Type::Var(a)],
                    Type::Var(a),
                ),
            },
        );

        // ----- List (Layer 1 primitives + Layer 3 composed) -----
        // list.length : List<a> → Int
        cat.add(
            "hash:list.length",
            TypeScheme {
                vars: vec![a],
                ty: Type::fun1(Type::list(Type::Var(a)), Type::int()),
            },
        );
        // list.map : (a → b, List<a>) → List<b>
        cat.add(
            "hash:list.map",
            TypeScheme {
                vars: vec![a, b],
                ty: Type::fun(
                    vec![
                        Type::fun1(Type::Var(a), Type::Var(b)),
                        Type::list(Type::Var(a)),
                    ],
                    Type::list(Type::Var(b)),
                ),
            },
        );
        // list.filter : (a → Boolean, List<a>) → List<a>
        cat.add(
            "hash:list.filter",
            TypeScheme {
                vars: vec![a],
                ty: Type::fun(
                    vec![
                        Type::fun1(Type::Var(a), Type::boolean()),
                        Type::list(Type::Var(a)),
                    ],
                    Type::list(Type::Var(a)),
                ),
            },
        );
        // list.fold_left : ((b, a) → b, b, List<a>) → b
        cat.add(
            "hash:list.fold_left",
            TypeScheme {
                vars: vec![a, b],
                ty: Type::fun(
                    vec![
                        Type::fun(vec![Type::Var(b), Type::Var(a)], Type::Var(b)),
                        Type::Var(b),
                        Type::list(Type::Var(a)),
                    ],
                    Type::Var(b),
                ),
            },
        );
        // list.sort_by_desc : (a → b, List<a>) → List<a>
        cat.add(
            "hash:list.sort_by_desc",
            TypeScheme {
                vars: vec![a, b],
                ty: Type::fun(
                    vec![
                        Type::fun1(Type::Var(a), Type::Var(b)),
                        Type::list(Type::Var(a)),
                    ],
                    Type::list(Type::Var(a)),
                ),
            },
        );
        // list.get : (Int, List<a>) → Maybe<a>
        cat.add(
            "hash:list.get",
            TypeScheme {
                vars: vec![a],
                ty: Type::fun(
                    vec![Type::int(), Type::list(Type::Var(a))],
                    Type::maybe(Type::Var(a)),
                ),
            },
        );
        // list.append : (a, List<a>) → List<a>
        cat.add(
            "hash:list.append",
            TypeScheme {
                vars: vec![a],
                ty: Type::fun(
                    vec![Type::Var(a), Type::list(Type::Var(a))],
                    Type::list(Type::Var(a)),
                ),
            },
        );
        // list.any : (a → Boolean, List<a>) → Boolean
        cat.add(
            "hash:list.any",
            TypeScheme {
                vars: vec![a],
                ty: Type::fun(
                    vec![
                        Type::fun1(Type::Var(a), Type::boolean()),
                        Type::list(Type::Var(a)),
                    ],
                    Type::boolean(),
                ),
            },
        );
        // list.is_empty : List<a> → Boolean
        cat.add(
            "hash:list.is_empty",
            TypeScheme {
                vars: vec![a],
                ty: Type::fun1(Type::list(Type::Var(a)), Type::boolean()),
            },
        );
        // list.concat : (List<a>, List<a>) → List<a>
        cat.add(
            "hash:list.concat",
            TypeScheme {
                vars: vec![a],
                ty: Type::fun(
                    vec![Type::list(Type::Var(a)), Type::list(Type::Var(a))],
                    Type::list(Type::Var(a)),
                ),
            },
        );

        // ----- Maybe (Layer 1/3) -----
        // maybe.map : (a → b, Maybe<a>) → Maybe<b>
        cat.add(
            "hash:maybe.map",
            TypeScheme {
                vars: vec![a, b],
                ty: Type::fun(
                    vec![
                        Type::fun1(Type::Var(a), Type::Var(b)),
                        Type::maybe(Type::Var(a)),
                    ],
                    Type::maybe(Type::Var(b)),
                ),
            },
        );
        // maybe.just : a → Maybe<a>
        cat.add(
            "hash:maybe.just",
            TypeScheme {
                vars: vec![a],
                ty: Type::fun1(Type::Var(a), Type::maybe(Type::Var(a))),
            },
        );

        // ----- String (Layer 1) -----
        // string.concat : (String, String) → String
        cat.add(
            "hash:string.concat",
            TypeScheme::mono(Type::fun(
                vec![Type::string(), Type::string()],
                Type::string(),
            )),
        );
        // string.length : String → Int
        cat.add(
            "hash:string.length",
            TypeScheme::mono(Type::fun1(Type::string(), Type::int())),
        );

        // ----- Record (Layer 1) -----
        // record.get : (String, { ... | r }) → Maybe<a>
        // This is polymorphic over the record type — simplified here
        cat.add(
            "hash:record.get",
            TypeScheme {
                vars: vec![a],
                ty: Type::fun(
                    vec![Type::string(), Type::Var(a)],
                    Type::maybe(Type::Var(b)),
                ),
            },
        );
        // record.set : (String, a, { ... | r }) → { ... | r }
        cat.add(
            "hash:record.set",
            TypeScheme {
                vars: vec![a, b],
                ty: Type::fun(
                    vec![Type::string(), Type::Var(a), Type::Var(b)],
                    Type::Var(b),
                ),
            },
        );
        // record.extend : (String, a, { ... | r }) → { ... | r }
        cat.add(
            "hash:record.extend",
            TypeScheme {
                vars: vec![a, b],
                ty: Type::fun(
                    vec![Type::string(), Type::Var(a), Type::Var(b)],
                    Type::Var(b),
                ),
            },
        );

        // ----- Tuple (Layer 1) -----
        // tuple.first : (a, b) → a
        cat.add(
            "hash:tuple.first",
            TypeScheme {
                vars: vec![a, b],
                ty: Type::fun1(Type::Tuple(vec![Type::Var(a), Type::Var(b)]), Type::Var(a)),
            },
        );
        // tuple.second : (a, b) → b
        cat.add(
            "hash:tuple.second",
            TypeScheme {
                vars: vec![a, b],
                ty: Type::fun1(Type::Tuple(vec![Type::Var(a), Type::Var(b)]), Type::Var(b)),
            },
        );
        // tuple.pair : (a, b) → (a, b)
        cat.add(
            "hash:tuple.pair",
            TypeScheme {
                vars: vec![a, b],
                ty: Type::fun(
                    vec![Type::Var(a), Type::Var(b)],
                    Type::Tuple(vec![Type::Var(a), Type::Var(b)]),
                ),
            },
        );

        // ----- Combinators (Layer 2) -----
        // compose : (b → c, a → b) → (a → c)
        cat.add(
            "hash:compose",
            TypeScheme {
                vars: vec![a, b, c],
                ty: Type::fun(
                    vec![
                        Type::fun1(Type::Var(b), Type::Var(c)),
                        Type::fun1(Type::Var(a), Type::Var(b)),
                    ],
                    Type::fun1(Type::Var(a), Type::Var(c)),
                ),
            },
        );
        // identity : a → a
        cat.add(
            "hash:identity",
            TypeScheme {
                vars: vec![a],
                ty: Type::fun1(Type::Var(a), Type::Var(a)),
            },
        );
        // fix : ((a → b) → (a → b)) → (a → b)
        cat.add(
            "hash:fix",
            TypeScheme {
                vars: vec![a, b],
                ty: Type::fun1(
                    Type::fun1(
                        Type::fun1(Type::Var(a), Type::Var(b)),
                        Type::fun1(Type::Var(a), Type::Var(b)),
                    ),
                    Type::fun1(Type::Var(a), Type::Var(b)),
                ),
            },
        );

        // ----- Math composed (Layer 3) -----
        // math.sum_float : List<Float> → Float
        cat.add(
            "hash:math.sum_float",
            TypeScheme::mono(Type::fun1(Type::list(Type::float()), Type::float())),
        );

        // ----- Date (Layer 1 domain) -----
        cat.add(
            "hash:date.gte",
            TypeScheme::mono(Type::fun(
                vec![Type::Con("Date".into(), vec![]), Type::Con("Date".into(), vec![])],
                Type::boolean(),
            )),
        );
        cat.add(
            "hash:date.subtract",
            TypeScheme::mono(Type::fun(
                vec![Type::Con("Date".into(), vec![]), Type::int()],
                Type::Con("Date".into(), vec![]),
            )),
        );

        cat
    }
}

// ---------------------------------------------------------------------------
// Helpers
// ---------------------------------------------------------------------------

fn rexpr(kind: RExprKind) -> RExpr {
    RExpr {
        kind,
        span: Span::default(),
    }
}

fn bound(index: usize, name: &str) -> RExpr {
    rexpr(RExprKind::BoundVar {
        index,
        name: name.into(),
    })
}

fn catalog(hash: &str, name: &str) -> RExpr {
    rexpr(RExprKind::CatalogRef {
        hash: hash.into(),
        name: name.into(),
    })
}

fn apply(func: RExpr, args: Vec<RExpr>) -> RExpr {
    rexpr(RExprKind::Apply {
        func: Box::new(func),
        args,
    })
}

fn lambda(params: Vec<&str>, body: RExpr) -> RExpr {
    rexpr(RExprKind::Lambda {
        params: params.into_iter().map(|s| s.into()).collect(),
        body: Box::new(body),
    })
}

fn let_in(name: &str, value: RExpr, body: RExpr) -> RExpr {
    rexpr(RExprKind::Let {
        name: name.into(),
        value: Box::new(value),
        body: Box::new(body),
    })
}

fn int_lit(n: i64) -> RExpr {
    rexpr(RExprKind::IntLit(n))
}

fn string_lit(s: &str) -> RExpr {
    rexpr(RExprKind::StringLit(s.into()))
}

fn bool_lit(b: bool) -> RExpr {
    rexpr(RExprKind::BoolLit(b))
}

fn nothing_lit() -> RExpr {
    rexpr(RExprKind::NothingLit)
}

fn list_lit(elems: Vec<RExpr>) -> RExpr {
    rexpr(RExprKind::ListLit(elems))
}

fn record_lit(fields: Vec<(&str, RExpr)>) -> RExpr {
    rexpr(RExprKind::RecordLit(
        fields.into_iter().map(|(k, v)| (k.into(), v)).collect(),
    ))
}

fn tuple_lit(elems: Vec<RExpr>) -> RExpr {
    rexpr(RExprKind::TupleLit(elems))
}

fn constructor(name: &str, args: Vec<RExpr>) -> RExpr {
    rexpr(RExprKind::Constructor {
        name: name.into(),
        args,
    })
}

fn match_expr(scrutinee: RExpr, arms: Vec<MatchArm>) -> RExpr {
    rexpr(RExprKind::Match {
        scrutinee: Box::new(scrutinee),
        arms,
    })
}

fn field_access(expr: RExpr, fields: Vec<&str>) -> RExpr {
    rexpr(RExprKind::FieldAccess {
        expr: Box::new(expr),
        fields: fields.into_iter().map(|s| s.into()).collect(),
    })
}

// ===================================================================
// Tests
// ===================================================================

// ---- Literal typing ----

#[test]
fn literal_int() {
    let cat = MockCatalog::new();
    let result = type_check(&cat, &int_lit(42));
    assert!(result.is_ok());
    assert_eq!(result.ty, Type::int());
}

#[test]
fn literal_float() {
    let cat = MockCatalog::new();
    let result = type_check(&cat, &rexpr(RExprKind::FloatLit(3.14)));
    assert!(result.is_ok());
    assert_eq!(result.ty, Type::float());
}

#[test]
fn literal_string() {
    let cat = MockCatalog::new();
    let result = type_check(&cat, &string_lit("hello"));
    assert!(result.is_ok());
    assert_eq!(result.ty, Type::string());
}

#[test]
fn literal_bool() {
    let cat = MockCatalog::new();
    let result = type_check(&cat, &bool_lit(true));
    assert!(result.is_ok());
    assert_eq!(result.ty, Type::boolean());
}

#[test]
fn literal_nothing() {
    let cat = MockCatalog::new();
    let result = type_check(&cat, &nothing_lit());
    assert!(result.is_ok());
    // Nothing : Maybe<a> — the element type is unconstrained
    match &result.ty {
        Type::Con(name, args) if name == "Maybe" && args.len() == 1 => {}
        other => panic!("Expected Maybe<a>, got {}", other),
    }
}

// ---- Identity lambda ----

#[test]
fn lambda_identity() {
    let cat = MockCatalog::new();
    // \(x). x
    let expr = lambda(vec!["x"], bound(0, "x"));
    let result = type_check(&cat, &expr);
    assert!(result.is_ok());
    // Should be a → a
    match &result.ty {
        Type::Fun(inputs, output) if inputs.len() == 1 => {
            assert_eq!(inputs[0], **output, "Identity should have same input and output type");
        }
        other => panic!("Expected a → a, got {}", other),
    }
}

// ---- Catalog function application ----

#[test]
fn apply_int_add() {
    let cat = MockCatalog::standard();
    // int.add(1, 2)
    let expr = apply(catalog("hash:int.add", "int.add"), vec![int_lit(1), int_lit(2)]);
    let result = type_check(&cat, &expr);
    assert!(result.is_ok(), "Errors: {:?}", result.errors);
    assert_eq!(result.ty, Type::int());
}

#[test]
fn apply_list_map() {
    let cat = MockCatalog::standard();
    // list.map(\(x). int.multiply(x, 2), [1, 2, 3])
    let mapper = lambda(
        vec!["x"],
        apply(
            catalog("hash:int.multiply", "int.multiply"),
            vec![bound(0, "x"), int_lit(2)],
        ),
    );
    let expr = apply(
        catalog("hash:list.map", "list.map"),
        vec![mapper, list_lit(vec![int_lit(1), int_lit(2), int_lit(3)])],
    );
    let result = type_check(&cat, &expr);
    assert!(result.is_ok(), "Errors: {:?}", result.errors);
    assert_eq!(result.ty, Type::list(Type::int()));
}

#[test]
fn apply_list_filter() {
    let cat = MockCatalog::standard();
    // list.filter(\(x). int.greater_than(x, 0), [1, -2, 3])
    let pred = lambda(
        vec!["x"],
        apply(
            catalog("hash:int.greater_than", "int.greater_than"),
            vec![bound(0, "x"), int_lit(0)],
        ),
    );
    let expr = apply(
        catalog("hash:list.filter", "list.filter"),
        vec![pred, list_lit(vec![int_lit(1), int_lit(-2), int_lit(3)])],
    );
    let result = type_check(&cat, &expr);
    assert!(result.is_ok(), "Errors: {:?}", result.errors);
    assert_eq!(result.ty, Type::list(Type::int()));
}

// ---- Let-polymorphism ----

#[test]
fn let_polymorphism() {
    let cat = MockCatalog::standard();
    // let id = \(x). x in (id(1), id("hello"))
    // id should be polymorphic: usable at both Int and String
    let id_fn = lambda(vec!["x"], bound(0, "x"));
    let body = tuple_lit(vec![
        apply(bound(0, "id"), vec![int_lit(1)]),
        apply(bound(0, "id"), vec![string_lit("hello")]),
    ]);
    let expr = let_in("id", id_fn, body);
    let result = type_check(&cat, &expr);
    assert!(result.is_ok(), "Let-polymorphism failed: {:?}", result.errors);
    match &result.ty {
        Type::Tuple(elems) if elems.len() == 2 => {
            assert_eq!(elems[0], Type::int());
            assert_eq!(elems[1], Type::string());
        }
        other => panic!("Expected (Int, String), got {}", other),
    }
}

// ---- math.mean composition ----

#[test]
fn math_mean_composition() {
    let cat = MockCatalog::standard();
    // λ(xs). float.divide(math.sum_float(xs), int.to_float(list.length(xs)))
    let expr = lambda(
        vec!["xs"],
        apply(
            catalog("hash:float.divide", "float.divide"),
            vec![
                apply(
                    catalog("hash:math.sum_float", "math.sum_float"),
                    vec![bound(0, "xs")],
                ),
                apply(
                    catalog("hash:int.to_float", "int.to_float"),
                    vec![apply(
                        catalog("hash:list.length", "list.length"),
                        vec![bound(0, "xs")],
                    )],
                ),
            ],
        ),
    );
    let result = type_check(&cat, &expr);
    assert!(result.is_ok(), "math.mean errors: {:?}", result.errors);
    // Should be List<Float> → Float
    match &result.ty {
        Type::Fun(inputs, output) if inputs.len() == 1 => {
            assert_eq!(inputs[0], Type::list(Type::float()));
            assert_eq!(**output, Type::float());
        }
        other => panic!("Expected List<Float> → Float, got {}", other),
    }
}

// ---- Nested filter/map/fold chain ----

#[test]
fn pipe_chain_desugared() {
    let cat = MockCatalog::standard();
    // Equivalent PFCL source (function-call form):
    // list.fold_left(int.add, 0,
    //   list.map(\(x). int.multiply(x, 2),
    //     list.filter(\(x). int.greater_than(x, 0), xs)))
    //
    // (Historical note: this test predates the |> retirement; the function
    // name is retained to keep CI history stable.)

    let pred = lambda(
        vec!["x"],
        apply(
            catalog("hash:int.greater_than", "int.greater_than"),
            vec![bound(0, "x"), int_lit(0)],
        ),
    );
    let mapper = lambda(
        vec!["x"],
        apply(
            catalog("hash:int.multiply", "int.multiply"),
            vec![bound(0, "x"), int_lit(2)],
        ),
    );

    let inner = lambda(
        vec!["xs"],
        apply(
            catalog("hash:list.fold_left", "list.fold_left"),
            vec![
                catalog("hash:int.add", "int.add"),
                int_lit(0),
                apply(
                    catalog("hash:list.map", "list.map"),
                    vec![
                        mapper,
                        apply(
                            catalog("hash:list.filter", "list.filter"),
                            vec![pred, bound(0, "xs")],
                        ),
                    ],
                ),
            ],
        ),
    );

    let result = type_check(&cat, &inner);
    assert!(result.is_ok(), "Pipe chain errors: {:?}", result.errors);
    // Should be List<Int> → Int
    match &result.ty {
        Type::Fun(inputs, output) if inputs.len() == 1 => {
            assert_eq!(inputs[0], Type::list(Type::int()));
            assert_eq!(**output, Type::int());
        }
        other => panic!("Expected List<Int> → Int, got {}", other),
    }
}

// ---- Let chains ----

#[test]
fn let_chain() {
    let cat = MockCatalog::standard();
    // let x = 1 in let y = 2 in int.add(x, y)
    let expr = let_in(
        "x",
        int_lit(1),
        let_in(
            "y",
            int_lit(2),
            apply(
                catalog("hash:int.add", "int.add"),
                vec![bound(1, "x"), bound(0, "y")],
            ),
        ),
    );
    let result = type_check(&cat, &expr);
    assert!(result.is_ok(), "Let chain errors: {:?}", result.errors);
    assert_eq!(result.ty, Type::int());
}

// ---- Match expression ----

#[test]
fn match_maybe() {
    let cat = MockCatalog::standard();
    // match m with
    // | Just(v) -> int.add(v, 1)
    // | Nothing -> 0
    //
    // where m : Maybe<Int>

    // Build as: \(m). match m with | Just(v) -> int.add(v, 1) | Nothing -> 0
    let expr = lambda(
        vec!["m"],
        match_expr(
            bound(0, "m"),
            vec![
                MatchArm {
                    pattern: Pattern::Constructor {
                        name: "Just".into(),
                        args: vec![Pattern::Var("v".into())],
                    },
                    body: apply(
                        catalog("hash:int.add", "int.add"),
                        vec![bound(0, "v"), int_lit(1)],
                    ),
                },
                MatchArm {
                    pattern: Pattern::NothingPat,
                    body: int_lit(0),
                },
            ],
        ),
    );

    let result = type_check(&cat, &expr);
    assert!(result.is_ok(), "Match errors: {:?}", result.errors);
    // Should be Maybe<Int> → Int
    match &result.ty {
        Type::Fun(inputs, output) if inputs.len() == 1 => {
            assert_eq!(inputs[0], Type::maybe(Type::int()));
            assert_eq!(**output, Type::int());
        }
        other => panic!("Expected Maybe<Int> → Int, got {}", other),
    }
}

// ---- List literal typing ----

#[test]
fn list_literal_homogeneous() {
    let cat = MockCatalog::new();
    let expr = list_lit(vec![int_lit(1), int_lit(2), int_lit(3)]);
    let result = type_check(&cat, &expr);
    assert!(result.is_ok());
    assert_eq!(result.ty, Type::list(Type::int()));
}

#[test]
fn list_literal_heterogeneous_error() {
    let cat = MockCatalog::new();
    let expr = list_lit(vec![int_lit(1), string_lit("oops")]);
    let result = type_check(&cat, &expr);
    assert!(!result.is_ok(), "Should detect heterogeneous list");
    assert!(!result.errors.is_empty());
}

#[test]
fn empty_list() {
    let cat = MockCatalog::new();
    let expr = list_lit(vec![]);
    let result = type_check(&cat, &expr);
    assert!(result.is_ok());
    // Empty list: List<a> for fresh a
    match &result.ty {
        Type::Con(name, args) if name == "List" && args.len() == 1 => {}
        other => panic!("Expected List<a>, got {}", other),
    }
}

// ---- Record literal ----

#[test]
fn record_literal() {
    let cat = MockCatalog::new();
    let expr = record_lit(vec![
        ("name", string_lit("Alice")),
        ("age", int_lit(30)),
    ]);
    let result = type_check(&cat, &expr);
    assert!(result.is_ok());
    match &result.ty {
        Type::Record(fields, None) => {
            assert_eq!(fields.len(), 2);
            assert_eq!(fields["name"], Type::string());
            assert_eq!(fields["age"], Type::int());
        }
        other => panic!("Expected record type, got {}", other),
    }
}

// ---- Tuple literal ----

#[test]
fn tuple_literal() {
    let cat = MockCatalog::new();
    let expr = tuple_lit(vec![int_lit(1), string_lit("hello"), bool_lit(true)]);
    let result = type_check(&cat, &expr);
    assert!(result.is_ok());
    assert_eq!(
        result.ty,
        Type::Tuple(vec![Type::int(), Type::string(), Type::boolean()])
    );
}

// ---- Constructor typing ----

#[test]
fn constructor_just() {
    let cat = MockCatalog::new();
    let expr = constructor("Just", vec![int_lit(42)]);
    let result = type_check(&cat, &expr);
    assert!(result.is_ok());
    assert_eq!(result.ty, Type::maybe(Type::int()));
}

#[test]
fn constructor_left() {
    let cat = MockCatalog::new();
    let expr = constructor("Left", vec![string_lit("error")]);
    let result = type_check(&cat, &expr);
    assert!(result.is_ok());
    match &result.ty {
        Type::Con(name, args) if name == "Either" && args.len() == 2 => {
            assert_eq!(args[0], Type::string());
            // Right type is unconstrained
        }
        other => panic!("Expected Either<String, b>, got {}", other),
    }
}

// ---- Error: arity mismatch ----

#[test]
fn error_arity_mismatch() {
    let cat = MockCatalog::standard();
    // int.add(1) — missing second argument
    let expr = apply(catalog("hash:int.add", "int.add"), vec![int_lit(1)]);
    let result = type_check(&cat, &expr);
    assert!(!result.is_ok(), "Should detect arity mismatch");
}

// ---- Error: type mismatch in application ----

#[test]
fn error_type_mismatch_arg() {
    let cat = MockCatalog::standard();
    // int.add(1, "hello") — wrong type for second arg
    let expr = apply(
        catalog("hash:int.add", "int.add"),
        vec![int_lit(1), string_lit("hello")],
    );
    let result = type_check(&cat, &expr);
    assert!(!result.is_ok(), "Should detect type mismatch");
}

// ---- Error: unknown catalog entry ----

#[test]
fn error_unknown_catalog() {
    let cat = MockCatalog::new(); // empty catalog!
    let expr = apply(catalog("hash:nonexistent", "nonexistent"), vec![int_lit(1)]);
    let result = type_check(&cat, &expr);
    assert!(!result.is_ok());
    // Should produce an UnknownCatalogEntry error
    assert!(result.errors.iter().any(|e| matches!(
        &e.kind,
        TypeErrorKind::UnknownCatalogEntry { .. }
    )));
}

// ---- Gap report formatting ----

#[test]
fn gap_report_well_typed() {
    let cat = MockCatalog::standard();
    let expr = apply(catalog("hash:int.add", "int.add"), vec![int_lit(1), int_lit(2)]);
    let result = type_check(&cat, &expr);
    let report = result.gap_report();
    assert!(report.starts_with("✓"), "Expected well-typed report, got: {}", report);
}

#[test]
fn gap_report_with_errors() {
    let cat = MockCatalog::standard();
    let expr = apply(
        catalog("hash:int.add", "int.add"),
        vec![int_lit(1), string_lit("oops")],
    );
    let result = type_check(&cat, &expr);
    let report = result.gap_report();
    assert!(report.starts_with("✗"), "Expected error report, got: {}", report);
    assert!(report.contains("type error"), "Report: {}", report);
}

// ---- Field access ----

#[test]
fn field_access_on_record() {
    let cat = MockCatalog::new();
    // \(r). r.name
    let expr = lambda(
        vec!["r"],
        field_access(bound(0, "r"), vec!["name"]),
    );
    let result = type_check(&cat, &expr);
    assert!(result.is_ok(), "Field access errors: {:?}", result.errors);
    // Should be { name: a | r } → a
    match &result.ty {
        Type::Fun(inputs, _output) if inputs.len() == 1 => {
            match &inputs[0] {
                Type::Record(fields, Some(_row)) => {
                    assert!(fields.contains_key("name"), "Record should have 'name' field");
                }
                _ => {} // The row type might get resolved differently
            }
        }
        other => panic!("Expected function, got {}", other),
    }
}

// ---- Nested lambdas ----

#[test]
fn nested_lambdas() {
    let cat = MockCatalog::standard();
    // \(x). \(y). int.add(x, y)
    let expr = lambda(
        vec!["x"],
        lambda(
            vec!["y"],
            apply(
                catalog("hash:int.add", "int.add"),
                vec![bound(1, "x"), bound(0, "y")],
            ),
        ),
    );
    let result = type_check(&cat, &expr);
    assert!(result.is_ok(), "Nested lambda errors: {:?}", result.errors);
    // Should be Int → (Int → Int)
    match &result.ty {
        Type::Fun(inputs, output) if inputs.len() == 1 => {
            assert_eq!(inputs[0], Type::int());
            match output.as_ref() {
                Type::Fun(inner_inputs, inner_output) if inner_inputs.len() == 1 => {
                    assert_eq!(inner_inputs[0], Type::int());
                    assert_eq!(**inner_output, Type::int());
                }
                other => panic!("Expected Int → Int, got {}", other),
            }
        }
        other => panic!("Expected Int → (Int → Int), got {}", other),
    }
}

// ---- compose combinator ----

#[test]
fn compose_combinator() {
    let cat = MockCatalog::standard();
    // compose(bool.not, \(x). int.greater_than(x, 0))
    // Should be: Int → Boolean
    let gt_zero = lambda(
        vec!["x"],
        apply(
            catalog("hash:int.greater_than", "int.greater_than"),
            vec![bound(0, "x"), int_lit(0)],
        ),
    );
    let expr = apply(
        catalog("hash:compose", "compose"),
        vec![catalog("hash:bool.not", "bool.not"), gt_zero],
    );
    let result = type_check(&cat, &expr);
    assert!(result.is_ok(), "compose errors: {:?}", result.errors);
    // Should be Int → Boolean
    match &result.ty {
        Type::Fun(inputs, output) if inputs.len() == 1 => {
            assert_eq!(inputs[0], Type::int());
            assert_eq!(**output, Type::boolean());
        }
        other => panic!("Expected Int → Boolean, got {}", other),
    }
}

// ---- Real catalog composition: list.map body ----
// list.map : \(f, xs). fold_right(\(x, acc). cons(f(x), acc), empty(), xs)
// (This is how list.map is composed in the catalog — but since list.map
// is a primitive, we test a similar composition pattern)

#[test]
fn maybe_map_in_context() {
    let cat = MockCatalog::standard();
    // \(idx, xs). maybe.map(\(x). int.add(x, 1), list.get(idx, xs))
    let expr = lambda(
        vec!["idx", "xs"],
        apply(
            catalog("hash:maybe.map", "maybe.map"),
            vec![
                lambda(
                    vec!["x"],
                    apply(
                        catalog("hash:int.add", "int.add"),
                        vec![bound(0, "x"), int_lit(1)],
                    ),
                ),
                apply(
                    catalog("hash:list.get", "list.get"),
                    vec![bound(0, "idx"), bound(1, "xs")],
                ),
            ],
        ),
    );
    let result = type_check(&cat, &expr);
    assert!(result.is_ok(), "maybe.map errors: {:?}", result.errors);
    // Should be (Int, List<Int>) → Maybe<Int>
    match &result.ty {
        Type::Fun(inputs, output) if inputs.len() == 2 => {
            assert_eq!(inputs[0], Type::int());
            assert_eq!(inputs[1], Type::list(Type::int()));
            assert_eq!(**output, Type::maybe(Type::int()));
        }
        other => panic!("Expected (Int, List<Int>) → Maybe<Int>, got {}", other),
    }
}

// ---- Higher-order composition: map then filter ----

#[test]
fn higher_order_map_filter() {
    let cat = MockCatalog::standard();
    // \(xs).
    //   let doubled = list.map(\(x). int.multiply(x, 2), xs) in
    //   list.filter(\(x). int.greater_than(x, 5), doubled)
    let expr = lambda(
        vec!["xs"],
        let_in(
            "doubled",
            apply(
                catalog("hash:list.map", "list.map"),
                vec![
                    lambda(
                        vec!["x"],
                        apply(
                            catalog("hash:int.multiply", "int.multiply"),
                            vec![bound(0, "x"), int_lit(2)],
                        ),
                    ),
                    bound(0, "xs"),
                ],
            ),
            apply(
                catalog("hash:list.filter", "list.filter"),
                vec![
                    lambda(
                        vec!["x"],
                        apply(
                            catalog("hash:int.greater_than", "int.greater_than"),
                            vec![bound(0, "x"), int_lit(5)],
                        ),
                    ),
                    bound(0, "doubled"),
                ],
            ),
        ),
    );
    let result = type_check(&cat, &expr);
    assert!(result.is_ok(), "map-filter errors: {:?}", result.errors);
    // Should be List<Int> → List<Int>
    match &result.ty {
        Type::Fun(inputs, output) if inputs.len() == 1 => {
            assert_eq!(inputs[0], Type::list(Type::int()));
            assert_eq!(**output, Type::list(Type::int()));
        }
        other => panic!("Expected List<Int> → List<Int>, got {}", other),
    }
}

// ---- Match with tuple pattern ----

#[test]
fn match_tuple_pattern() {
    let cat = MockCatalog::standard();
    // \(pair). match pair with | (a, b) -> int.add(a, b)
    let expr = lambda(
        vec!["pair"],
        match_expr(
            bound(0, "pair"),
            vec![MatchArm {
                pattern: Pattern::TuplePat(vec![
                    Pattern::Var("a".into()),
                    Pattern::Var("b".into()),
                ]),
                body: apply(
                    catalog("hash:int.add", "int.add"),
                    vec![bound(0, "a"), bound(1, "b")],
                ),
            }],
        ),
    );
    let result = type_check(&cat, &expr);
    assert!(result.is_ok(), "Tuple match errors: {:?}", result.errors);
    // Should be (Int, Int) → Int
    match &result.ty {
        Type::Fun(inputs, output) if inputs.len() == 1 => {
            assert_eq!(inputs[0], Type::Tuple(vec![Type::int(), Type::int()]));
            assert_eq!(**output, Type::int());
        }
        other => panic!("Expected (Int, Int) → Int, got {}", other),
    }
}

// ---- Record with lambda values ----

#[test]
fn record_with_lambda_values() {
    let cat = MockCatalog::standard();
    // { inc: \(x). int.add(x, 1), dec: \(x). int.subtract(x, 1) }
    let expr = record_lit(vec![
        (
            "inc",
            lambda(
                vec!["x"],
                apply(
                    catalog("hash:int.add", "int.add"),
                    vec![bound(0, "x"), int_lit(1)],
                ),
            ),
        ),
        (
            "dec",
            lambda(
                vec!["x"],
                apply(
                    catalog("hash:int.subtract", "int.subtract"),
                    vec![bound(0, "x"), int_lit(1)],
                ),
            ),
        ),
    ]);
    let result = type_check(&cat, &expr);
    assert!(result.is_ok(), "Record with lambdas errors: {:?}", result.errors);
    match &result.ty {
        Type::Record(fields, None) => {
            assert_eq!(fields.len(), 2);
            assert_eq!(
                fields["inc"],
                Type::fun(vec![Type::int()], Type::int())
            );
            assert_eq!(
                fields["dec"],
                Type::fun(vec![Type::int()], Type::int())
            );
        }
        other => panic!("Expected record type, got {}", other),
    }
}
