//! Pin for the iter-24.3 codegen `import_map`-fallback path
//! (design/contracts/0013-typeclasses.md, "Cross-module references in
//! synthesised bodies" invariant 2).
//!
//! Property protected: post-mono synthesised body cross-module
//! references resolve at codegen via the fallback to
//! `module_user_fns` / `module_def_ail_types` when the prefix is
//! NOT in the current module's `import_map`. Specifically, the
//! synthesised `prelude.print__<UserType>` body references
//! `<user_module>.show__<UserType>` even though `prelude` does not
//! import user modules.
//!
//! Failure mode this pin catches: a future codegen refactor
//! tightens `resolve_top_level_fn` or `lower_app`'s cross-module
//! arm or `synth_with_extras`'s Var arm back to `import_map`-only.
//! Without this pin, the regression surfaces only at the
//! `show_user_adt` E2E (which builds + runs a binary, slow to
//! bisect).

use ailang_check::{check_workspace, monomorphise_workspace};
use ailang_core::ast::{Def, Term};
use ailang_surface::load_workspace;
use std::path::PathBuf;

fn fixture_path() -> PathBuf {
    PathBuf::from(env!("CARGO_MANIFEST_DIR"))
        .join("../../examples")
        .join("show_user_adt.ail")
}

#[test]
fn synthesised_print_uses_user_module_show_via_fallback() {
    // Step 1: workspace loads + typechecks clean.
    let ws = load_workspace(&fixture_path()).expect("workspace loads");
    let diags = check_workspace(&ws);
    assert!(
        diags.is_empty(),
        "typecheck diagnostics in show_user_adt fixture: {diags:?}"
    );

    // Step 2: mono synthesis produces `prelude.print__<IntBox>` whose
    // body references `show_user_adt.show__<IntBox>` (cross-module).
    let post_mono = monomorphise_workspace(&ws).expect("mono green");
    let prelude_mod = post_mono
        .modules
        .get("prelude")
        .expect("prelude post-mono module present");

    let print_def = prelude_mod
        .defs
        .iter()
        .find_map(|d| match d {
            Def::Fn(f) if f.name.starts_with("print__") => Some(f),
            _ => None,
        })
        .expect("synthesised print__<UserType> not found in prelude post-mono module");

    // Step 3: recursively walk `print_def.body` looking for a Var
    // whose name carries the `show_user_adt.` prefix (the cross-
    // module reference invariant 2 protects).
    fn contains_xmod_show_var(t: &Term) -> bool {
        match t {
            Term::Var { name } => {
                name.starts_with("show_user_adt.") && name.contains("show__")
            }
            Term::Let { value, body, .. } => {
                contains_xmod_show_var(value) || contains_xmod_show_var(body)
            }
            Term::LetRec { body, in_term, .. } => {
                contains_xmod_show_var(body) || contains_xmod_show_var(in_term)
            }
            Term::App { callee, args, .. } => {
                contains_xmod_show_var(callee) || args.iter().any(contains_xmod_show_var)
            }
            Term::Do { args, .. } => args.iter().any(contains_xmod_show_var),
            Term::Lam { body, .. } => contains_xmod_show_var(body),
            Term::If { cond, then, else_ } => {
                contains_xmod_show_var(cond)
                    || contains_xmod_show_var(then)
                    || contains_xmod_show_var(else_)
            }
            Term::Match { scrutinee, arms } => {
                contains_xmod_show_var(scrutinee)
                    || arms.iter().any(|a| contains_xmod_show_var(&a.body))
            }
            Term::Ctor { args, .. } => args.iter().any(contains_xmod_show_var),
            Term::Seq { lhs, rhs } => {
                contains_xmod_show_var(lhs) || contains_xmod_show_var(rhs)
            }
            Term::Clone { value } => contains_xmod_show_var(value),
            Term::ReuseAs { source, body } => {
                contains_xmod_show_var(source) || contains_xmod_show_var(body)
            }
            // loop-recur iter 1: a `Term::Loop` cannot itself host a
            // synthesised cross-module reference, but recurse
            // defensively through binder inits / body / recur args.
            Term::Loop { binders, body } => {
                binders.iter().any(|b| contains_xmod_show_var(&b.init))
                    || contains_xmod_show_var(body)
            }
            Term::Recur { args } => args.iter().any(contains_xmod_show_var),
            // prep.2 (kernel-extension-mechanics): recurse through
            // NewArg::Value subterms; type-args do not carry a Var.
            Term::New { args, .. } => args.iter().any(|arg| match arg {
                ailang_core::ast::NewArg::Value(v) => contains_xmod_show_var(v),
                ailang_core::ast::NewArg::Type(_) => false,
            }),
            Term::Lit { .. } => false,
            Term::Intrinsic => false,
        }
    }

    assert!(
        contains_xmod_show_var(&print_def.body),
        "synthesised print body should contain a `show_user_adt.<suffix>` Var \
         referencing the user-module's show__<IntBox> mono symbol — \
         this is the cross-module reference codegen resolves via the \
         import_map-fallback path. Body: {:?}",
        print_def.body
    );

    // Step 4: confirm prelude module's `imports` does NOT contain
    // `show_user_adt` — the resolution at codegen time genuinely
    // bypasses the source template's import_map.
    let prelude_src = ws
        .modules
        .get("prelude")
        .expect("prelude source module present");
    assert!(
        prelude_src
            .imports
            .iter()
            .all(|imp| imp.module != "show_user_adt"),
        "prelude must not import show_user_adt (the invariant is that \
         codegen resolves the cross-module ref WITHOUT going through \
         import_map). Got imports: {:?}",
        prelude_src.imports
    );
}