// ============================================================================
// PFCL Type Checker
// ============================================================================
//
// Stage 3 of the PFCL compiler pipeline:
//
//   PFCL source
//       │ parse()
//       ▼
//   Expr (unresolved AST)          ← Parser output
//       │ resolve(&catalog, &expr)
//       ▼
//   RExpr (resolved AST)           ← Resolver output
//       │ type_check(&catalog, &rexpr)
//       ▼
//   TExpr (typed AST)              ← THIS MODULE's output
//       │ emit_closure_graph()
//       ▼
//   ClosureNode                    ← Runtime execution target
//
// The type checker uses Hindley-Milner type inference (Algorithm W) with
// the catalog's function signatures as the type environment. It either
// proves a composition is well-typed (returning a typed AST with inferred
// types on every node) or produces a gap report listing what's missing.
//
// This crate is `no_std` compatible.

#![cfg_attr(not(feature = "std"), no_std)]

extern crate alloc;

// Re-export alloc types for internal use
pub(crate) use alloc::{boxed::Box, string::String, string::ToString, vec, vec::Vec};
pub(crate) use alloc::collections::{BTreeMap, BTreeSet};

pub mod types;
pub mod unify;
pub mod infer;
pub mod app_types;

// Re-export main public types
pub use types::{Type, TypeScheme, TypeVar, Substitution, FreshSupply};
pub use unify::{unify, TypeError, TypeErrorKind, ErrorContext};
pub use infer::{
    RExpr, RExprKind, Span, MatchArm, Pattern,
    TExpr, TExprKind, TypedMatchArm,
    CatalogTypes, Inferencer, TypeCheckResult,
};
pub use app_types::{
    app_compose_scheme, app_compose_shared_scheme, app_with_config_scheme,
    is_app_intrinsic, app_intrinsic_scheme,
};

/// Convenience entry point: type-check a resolved expression against a catalog.
pub fn type_check<C: CatalogTypes>(catalog: &C, expr: &RExpr) -> TypeCheckResult {
    let inferencer = Inferencer::new(catalog);
    inferencer.check(expr)
}
