//! Pretty-printer for form (A).
//!
//! Mirrors the parser in [`mod@crate::parse`]. Output is deterministic
//! and parseable by the parser — round-trip is the gating contract
//! (see `tests/round_trip.rs`).
//!
//! Indentation is informational only (the lexer ignores it). Two-space
//! per level. Comments are NOT emitted.

use ailang_core::ast::{
    Arm, ClassDef, ClassMethod, Constraint, ConstDef, Ctor, Def, FnDef, Import, InstanceDef,
    InstanceMethod, Literal, Module, ParamMode, Pattern, SuperclassRef, Suppress, Term,
    Type, TypeDef,
};

/// Print a module in form (A).
pub fn print(module: &Module) -> String {
    let mut out = String::new();
    out.push('(');
    out.push_str("module ");
    out.push_str(&module.name);
    for imp in &module.imports {
        out.push('\n');
        write_import(&mut out, imp, 1);
    }
    for def in &module.defs {
        out.push('\n');
        write_def(&mut out, def, 1);
    }
    out.push(')');
    out.push('\n');
    out
}

/// Print a single [`Term`] in form (A) — the dual of
/// [`crate::parse::parse_term`]. Used by callers that produce form-A
/// snippets out-of-band, e.g. the `suggested_rewrites` payload of
/// `ail check --json` (Iter 18c.2). The output is round-trip stable
/// (`parse_term(term_to_form_a(t)) ≡ t`) but does not include a trailing
/// newline; callers that want one append it themselves.
pub fn term_to_form_a(t: &Term) -> String {
    let mut out = String::new();
    write_term(&mut out, t, 0);
    out
}

/// Iter 19a: render a [`Type`] as form-A. Used by diagnostics that want
/// to suggest a relaxed signature (e.g. `over-strict-mode` shows the
/// `(fn-type ...)` with `(borrow T)` in place of `(own T)`). Output is
/// the same shape that appears as the `type` slot of a `(fn ...)` def.
pub fn type_to_form_a(t: &Type) -> String {
    let mut out = String::new();
    write_type(&mut out, t);
    out
}

// ---- helpers --------------------------------------------------------------

fn indent(out: &mut String, level: usize) {
    for _ in 0..level {
        out.push_str("  ");
    }
}

fn write_string_lit(out: &mut String, s: &str) {
    out.push('"');
    for c in s.chars() {
        match c {
            '"' => out.push_str("\\\""),
            '\\' => out.push_str("\\\\"),
            '\n' => out.push_str("\\n"),
            '\t' => out.push_str("\\t"),
            '\r' => out.push_str("\\r"),
            other => out.push(other),
        }
    }
    out.push('"');
}

// ---- imports & defs -------------------------------------------------------

fn write_import(out: &mut String, imp: &Import, level: usize) {
    indent(out, level);
    out.push_str("(import ");
    out.push_str(&imp.module);
    if let Some(alias) = &imp.alias {
        out.push_str(" as ");
        out.push_str(alias);
    }
    out.push(')');
}

fn write_def(out: &mut String, def: &Def, level: usize) {
    match def {
        Def::Type(td) => write_type_def(out, td, level),
        Def::Fn(fd) => write_fn_def(out, fd, level),
        Def::Const(cd) => write_const_def(out, cd, level),
        Def::Class(c) => write_class_def(out, c, level),
        Def::Instance(i) => write_instance_def(out, i, level),
    }
}

fn write_type_def(out: &mut String, td: &TypeDef, level: usize) {
    indent(out, level);
    out.push_str("(data ");
    out.push_str(&td.name);
    if !td.vars.is_empty() {
        out.push_str(" (vars");
        for v in &td.vars {
            out.push(' ');
            out.push_str(v);
        }
        out.push(')');
    }
    if let Some(doc) = &td.doc {
        out.push('\n');
        indent(out, level + 1);
        out.push_str("(doc ");
        write_string_lit(out, doc);
        out.push(')');
    }
    for c in &td.ctors {
        out.push('\n');
        write_ctor(out, c, level + 1);
    }
    // Iter 18e: `(drop-iterative)` annotation. Printed last (after
    // every ctor) so the canonical form lands consistent with the
    // DESIGN.md example. Omitted when `drop_iterative == false`.
    if td.drop_iterative {
        out.push('\n');
        indent(out, level + 1);
        out.push_str("(drop-iterative)");
    }
    out.push(')');
}

fn write_ctor(out: &mut String, c: &Ctor, level: usize) {
    indent(out, level);
    out.push_str("(ctor ");
    out.push_str(&c.name);
    for f in &c.fields {
        out.push(' ');
        write_type(out, f);
    }
    out.push(')');
}

fn write_fn_def(out: &mut String, fd: &FnDef, level: usize) {
    indent(out, level);
    out.push_str("(fn ");
    out.push_str(&fd.name);
    if let Some(doc) = &fd.doc {
        out.push('\n');
        indent(out, level + 1);
        out.push_str("(doc ");
        write_string_lit(out, doc);
        out.push(')');
    }
    // Iter 19b: emit one `(suppress ...)` clause per entry, after the
    // doc string and before the type. Round-trip stable: parser
    // re-reads each clause back into [`FnDef::suppress`].
    for s in &fd.suppress {
        out.push('\n');
        write_suppress(out, s, level + 1);
    }
    out.push('\n');
    indent(out, level + 1);
    out.push_str("(type ");
    write_type(out, &fd.ty);
    out.push(')');
    out.push('\n');
    indent(out, level + 1);
    out.push_str("(params");
    for p in &fd.params {
        out.push(' ');
        out.push_str(p);
    }
    out.push(')');
    out.push('\n');
    indent(out, level + 1);
    out.push_str("(body ");
    write_term(out, &fd.body, level + 2);
    out.push(')');
    out.push(')');
}

/// Iter 19b: print one `(suppress (code "<c>") (because "<r>"))`
/// clause. Indentation matches the rest of the fn-def (one level
/// deeper than the `(fn ...)` head).
fn write_suppress(out: &mut String, s: &Suppress, level: usize) {
    indent(out, level);
    out.push_str("(suppress (code ");
    write_string_lit(out, &s.code);
    out.push_str(") (because ");
    write_string_lit(out, &s.because);
    out.push_str("))");
}

fn write_const_def(out: &mut String, cd: &ConstDef, level: usize) {
    indent(out, level);
    out.push_str("(const ");
    out.push_str(&cd.name);
    if let Some(doc) = &cd.doc {
        out.push('\n');
        indent(out, level + 1);
        out.push_str("(doc ");
        write_string_lit(out, doc);
        out.push(')');
    }
    out.push('\n');
    indent(out, level + 1);
    out.push_str("(type ");
    write_type(out, &cd.ty);
    out.push(')');
    out.push('\n');
    indent(out, level + 1);
    out.push_str("(body ");
    write_term(out, &cd.value, level + 2);
    out.push(')');
    out.push(')');
}

fn write_class_def(out: &mut String, c: &ClassDef, level: usize) {
    indent(out, level);
    out.push_str("(class ");
    out.push_str(&c.name);
    out.push('\n');
    indent(out, level + 1);
    out.push_str("(param ");
    out.push_str(&c.param);
    out.push(')');
    if let Some(sc) = &c.superclass {
        out.push('\n');
        write_superclass(out, sc, level + 1);
    }
    if let Some(doc) = &c.doc {
        out.push('\n');
        indent(out, level + 1);
        out.push_str("(doc ");
        write_string_lit(out, doc);
        out.push(')');
    }
    for m in &c.methods {
        out.push('\n');
        write_class_method(out, m, level + 1);
    }
    out.push(')');
}

fn write_superclass(out: &mut String, sc: &SuperclassRef, level: usize) {
    indent(out, level);
    out.push_str("(superclass (class ");
    out.push_str(&sc.class);
    out.push_str(") (type ");
    out.push_str(&sc.type_);
    out.push_str("))");
}

fn write_class_method(out: &mut String, m: &ClassMethod, level: usize) {
    indent(out, level);
    out.push_str("(method ");
    out.push_str(&m.name);
    out.push('\n');
    indent(out, level + 1);
    out.push_str("(type ");
    write_type(out, &m.ty);
    out.push(')');
    if let Some(default) = &m.default {
        out.push('\n');
        indent(out, level + 1);
        out.push_str("(default ");
        write_term(out, default, level + 2);
        out.push(')');
    }
    out.push(')');
}

fn write_instance_def(out: &mut String, i: &InstanceDef, level: usize) {
    indent(out, level);
    out.push_str("(instance");
    out.push('\n');
    indent(out, level + 1);
    out.push_str("(class ");
    out.push_str(&i.class);
    out.push(')');
    out.push('\n');
    indent(out, level + 1);
    out.push_str("(type ");
    write_type(out, &i.type_);
    out.push(')');
    if let Some(doc) = &i.doc {
        out.push('\n');
        indent(out, level + 1);
        out.push_str("(doc ");
        write_string_lit(out, doc);
        out.push(')');
    }
    for m in &i.methods {
        out.push('\n');
        write_instance_method(out, m, level + 1);
    }
    out.push(')');
}

fn write_instance_method(out: &mut String, m: &InstanceMethod, level: usize) {
    indent(out, level);
    out.push_str("(method ");
    out.push_str(&m.name);
    out.push('\n');
    indent(out, level + 1);
    out.push_str("(body ");
    write_term(out, &m.body, level + 2);
    out.push(')');
    out.push(')');
}

// ---- types ----------------------------------------------------------------

/// Iter 18a: print one fn-type param/ret slot, wrapping with
/// `(borrow ...)` or `(own ...)` when the slot has an explicit
/// mode. `Implicit` is printed bare so pre-18a fixtures round-trip
/// unchanged.
fn write_fn_type_slot(out: &mut String, t: &Type, mode: ParamMode) {
    match mode {
        ParamMode::Implicit => write_type(out, t),
        ParamMode::Own => {
            out.push_str("(own ");
            write_type(out, t);
            out.push(')');
        }
        ParamMode::Borrow => {
            out.push_str("(borrow ");
            write_type(out, t);
            out.push(')');
        }
    }
}

/// Iter 22b.4a.4.5: print one `(constraint <Class> <type>)` pair, used
/// inside the optional `(constraints …)` clause of a `(forall …)`. The
/// clause itself is omitted entirely when `Type::Forall.constraints` is
/// empty so pre-22b.2 forall fixtures stay bit-identical.
fn write_constraint(out: &mut String, c: &Constraint) {
    out.push_str("(constraint ");
    out.push_str(&c.class);
    out.push(' ');
    write_type(out, &c.type_);
    out.push(')');
}

fn write_type(out: &mut String, t: &Type) {
    match t {
        Type::Var { name } => out.push_str(name),
        Type::Con { name, args } => {
            out.push_str("(con ");
            out.push_str(name);
            for a in args {
                out.push(' ');
                write_type(out, a);
            }
            out.push(')');
        }
        Type::Fn {
            params,
            param_modes,
            ret,
            ret_mode,
            effects,
        } => {
            out.push_str("(fn-type (params");
            for (i, p) in params.iter().enumerate() {
                out.push(' ');
                let mode = param_modes.get(i).copied().unwrap_or(ParamMode::Implicit);
                write_fn_type_slot(out, p, mode);
            }
            out.push_str(") (ret ");
            write_fn_type_slot(out, ret, *ret_mode);
            out.push(')');
            if !effects.is_empty() {
                out.push_str(" (effects");
                for e in effects {
                    out.push(' ');
                    out.push_str(e);
                }
                out.push(')');
            }
            out.push(')');
        }
        Type::Forall { vars, constraints, body } => {
            out.push_str("(forall (vars");
            for v in vars {
                out.push(' ');
                out.push_str(v);
            }
            out.push(')');
            if !constraints.is_empty() {
                out.push_str(" (constraints");
                for c in constraints {
                    out.push(' ');
                    write_constraint(out, c);
                }
                out.push(')');
            }
            out.push(' ');
            write_type(out, body);
            out.push(')');
        }
    }
}

// ---- terms ----------------------------------------------------------------

fn write_term(out: &mut String, t: &Term, level: usize) {
    match t {
        Term::Lit { lit } => write_lit(out, lit),
        Term::Var { name } => out.push_str(name),
        Term::App { callee, args, tail } => {
            // Iter 14e: `tail-app` is the form for `App { tail: true }`;
            // otherwise the regular `app` head is used. Both productions
            // are positional analogues of each other — only the head
            // keyword differs.
            out.push_str(if *tail { "(tail-app " } else { "(app " });
            write_term(out, callee, level);
            for a in args {
                out.push(' ');
                write_term(out, a, level);
            }
            out.push(')');
        }
        Term::Let { name, value, body } => {
            out.push_str("(let ");
            out.push_str(name);
            out.push(' ');
            write_term(out, value, level);
            out.push(' ');
            write_term(out, body, level);
            out.push(')');
        }
        Term::LetRec { name, ty, params, body, in_term } => {
            out.push_str("(let-rec ");
            out.push_str(name);
            out.push_str(" (params");
            for p in params {
                out.push(' ');
                out.push_str(p);
            }
            out.push_str(") (type ");
            write_type(out, ty);
            out.push_str(") (body ");
            write_term(out, body, level);
            out.push_str(") (in ");
            write_term(out, in_term, level);
            out.push_str("))");
        }
        Term::If { cond, then, else_ } => {
            out.push_str("(if ");
            write_term(out, cond, level);
            out.push(' ');
            write_term(out, then, level);
            out.push(' ');
            write_term(out, else_, level);
            out.push(')');
        }
        Term::Do { op, args, tail } => {
            // Iter 14e: `tail-do` mirrors `tail-app` for effect ops.
            out.push_str(if *tail { "(tail-do " } else { "(do " });
            out.push_str(op);
            for a in args {
                out.push(' ');
                write_term(out, a, level);
            }
            out.push(')');
        }
        Term::Ctor { type_name, ctor, args } => {
            out.push_str("(term-ctor ");
            out.push_str(type_name);
            out.push(' ');
            out.push_str(ctor);
            for a in args {
                out.push(' ');
                write_term(out, a, level);
            }
            out.push(')');
        }
        Term::Match { scrutinee, arms } => {
            out.push_str("(match ");
            write_term(out, scrutinee, level);
            for arm in arms {
                out.push('\n');
                indent(out, level);
                write_arm(out, arm, level);
            }
            out.push(')');
        }
        Term::Lam {
            params,
            param_tys,
            ret_ty,
            effects,
            body,
        } => {
            out.push_str("(lam (params");
            for (name, ty) in params.iter().zip(param_tys.iter()) {
                out.push_str(" (typed ");
                out.push_str(name);
                out.push(' ');
                write_type(out, ty);
                out.push(')');
            }
            out.push_str(") (ret ");
            write_type(out, ret_ty);
            out.push(')');
            if !effects.is_empty() {
                out.push_str(" (effects");
                for e in effects {
                    out.push(' ');
                    out.push_str(e);
                }
                out.push(')');
            }
            out.push_str(" (body ");
            write_term(out, body, level);
            out.push_str("))");
        }
        Term::Seq { lhs, rhs } => {
            out.push_str("(seq ");
            write_term(out, lhs, level);
            out.push(' ');
            write_term(out, rhs, level);
            out.push(')');
        }
        Term::Clone { value } => {
            // Iter 18c.1: print as `(clone <inner>)`. The wrapper is
            // identity at typecheck/codegen in 18c.1; only authored
            // intent is recorded for the future inc/dec emission pass.
            out.push_str("(clone ");
            write_term(out, value, level);
            out.push(')');
        }
        Term::ReuseAs { source, body } => {
            // Iter 18d.1: print as `(reuse-as <source> <body>)`. The
            // wrapper is identity at codegen in 18d.1 (the `body` is
            // lowered, the `source` is dropped); 18d.2 will lower this
            // as in-place rewrite under `--alloc=rc`.
            out.push_str("(reuse-as ");
            write_term(out, source, level);
            out.push(' ');
            write_term(out, body, level);
            out.push(')');
        }
    }
}

fn write_arm(out: &mut String, arm: &Arm, level: usize) {
    out.push_str("(case ");
    write_pattern(out, &arm.pat);
    out.push(' ');
    write_term(out, &arm.body, level + 1);
    out.push(')');
}

/// Render a Float literal's bit pattern as surface text. The output
/// is the shortest round-trippable decimal produced by
/// `f64::to_string` (Grisu3). If the rendered form contains
/// neither `.` nor `e`/`E` (`f64::to_string` returns "1" for
/// `1.0_f64`, "10000000000" for `1e10_f64`), append `.0` so the
/// lexer's `is_int`/`has_dot|has_exp` dispatch routes the token to
/// the Float path on re-lex. This preserves the
/// `lex(print(L)) == L` round-trip property pinned by
/// [`print_then_parse_round_trip_float_literal`].
///
/// Non-finite bit patterns (NaN, ±Inf) cannot be expressed in
/// surface form (per spec section A2 — the lexer rejects all such
/// inputs). A Float literal in the AST whose bits are non-finite
/// must therefore have arrived via Form-A directly. The printer's
/// job is surface output, not a Form-A escape hatch, so we panic
/// rather than emit a non-round-trippable token.
fn write_float_lit(out: &mut String, bits: u64) {
    let f = f64::from_bits(bits);
    if !f.is_finite() {
        panic!(
            "write_float_lit: non-finite Float literal {bits:#018x} \
             cannot be expressed in surface form"
        );
    }
    let s = f.to_string();
    out.push_str(&s);
    if !s.contains('.') && !s.contains('e') && !s.contains('E') {
        out.push_str(".0");
    }
}

fn write_lit(out: &mut String, lit: &Literal) {
    match lit {
        Literal::Int { value } => out.push_str(&value.to_string()),
        Literal::Bool { value } => out.push_str(if *value { "true" } else { "false" }),
        Literal::Str { value } => write_string_lit(out, value),
        Literal::Unit => out.push_str("(lit-unit)"),
        Literal::Float { bits } => write_float_lit(out, *bits),
    }
}

fn write_pattern(out: &mut String, p: &Pattern) {
    match p {
        Pattern::Wild => out.push('_'),
        Pattern::Var { name } => out.push_str(name),
        Pattern::Lit { lit } => {
            out.push_str("(pat-lit ");
            // Inside pat-lit, write the bare literal form (no `(lit-unit)`
            // — Unit is not allowed in pat-lit per the grammar).
            match lit {
                Literal::Int { value } => out.push_str(&value.to_string()),
                Literal::Bool { value } => out.push_str(if *value { "true" } else { "false" }),
                Literal::Str { value } => write_string_lit(out, value),
                Literal::Unit => {
                    // Unit is not a valid pat-lit; fall back to a bare unit-lit
                    // form. This is unreachable for any well-formed AST that
                    // came through the typechecker.
                    out.push_str("(lit-unit)");
                }
                Literal::Float { bits } => write_float_lit(out, *bits),
            }
            out.push(')');
        }
        Pattern::Ctor { ctor, fields } => {
            out.push_str("(pat-ctor ");
            out.push_str(ctor);
            for f in fields {
                out.push(' ');
                write_pattern(out, f);
            }
            out.push(')');
        }
    }
}

#[cfg(test)]
mod tests {
    use super::*;

    fn round_trip(m: Module, label: &str) {
        let printed = print(&m);
        let parsed = crate::parse::parse(&printed)
            .unwrap_or_else(|e| panic!(
                "{label}: re-parse failed: {e:?}\nprinted:\n{printed}"
            ));
        let bytes_orig = ailang_core::canonical::to_bytes(&m);
        let bytes_back = ailang_core::canonical::to_bytes(&parsed);
        if bytes_orig != bytes_back {
            let s_orig = String::from_utf8_lossy(&bytes_orig).into_owned();
            let s_back = String::from_utf8_lossy(&bytes_back).into_owned();
            panic!(
                "{label}: canonical bytes differ.\noriginal: {s_orig}\nround:    {s_back}\nprinted:\n{printed}"
            );
        }
    }

    #[test]
    fn print_then_parse_round_trip_minimal_class() {
        let m = Module {
            schema: ailang_core::SCHEMA.to_string(),
            name: "M".into(),
            imports: vec![],
            defs: vec![Def::Class(ClassDef {
                name: "Foo".into(),
                param: "a".into(),
                superclass: None,
                methods: vec![ClassMethod {
                    name: "m".into(),
                    ty: Type::Fn {
                        params: vec![Type::Var { name: "a".into() }],
                        param_modes: vec![ParamMode::Implicit],
                        ret: Box::new(Type::int()),
                        ret_mode: ParamMode::Implicit,
                        effects: vec![],
                    },
                    default: None,
                }],
                doc: None,
            })],
        };
        round_trip(m, "minimal_class");
    }

    #[test]
    fn print_then_parse_round_trip_class_with_superclass_and_default() {
        let m = Module {
            schema: ailang_core::SCHEMA.to_string(),
            name: "M".into(),
            imports: vec![],
            defs: vec![Def::Class(ClassDef {
                name: "Bar".into(),
                param: "a".into(),
                superclass: Some(SuperclassRef {
                    class: "Foo".into(),
                    type_: "a".into(),
                }),
                methods: vec![ClassMethod {
                    name: "m".into(),
                    ty: Type::Fn {
                        params: vec![Type::Var { name: "a".into() }],
                        param_modes: vec![ParamMode::Implicit],
                        ret: Box::new(Type::int()),
                        ret_mode: ParamMode::Implicit,
                        effects: vec![],
                    },
                    default: Some(Term::Lit { lit: Literal::Int { value: 0 } }),
                }],
                doc: Some("docline".into()),
            })],
        };
        round_trip(m, "class_with_superclass_and_default");
    }

    #[test]
    fn print_then_parse_round_trip_forall_with_constraint() {
        let m = Module {
            schema: ailang_core::SCHEMA.to_string(),
            name: "M".into(),
            imports: vec![],
            defs: vec![Def::Fn(ailang_core::ast::FnDef {
                name: "f".into(),
                ty: Type::Forall {
                    vars: vec!["a".into()],
                    constraints: vec![ailang_core::ast::Constraint {
                        class: "Show".into(),
                        type_: Type::Var { name: "a".into() },
                    }],
                    body: Box::new(Type::Fn {
                        params: vec![Type::Var { name: "a".into() }],
                        param_modes: vec![ParamMode::Implicit],
                        ret: Box::new(Type::Con {
                            name: "Str".into(),
                            args: vec![],
                        }),
                        ret_mode: ParamMode::Implicit,
                        effects: vec![],
                    }),
                },
                params: vec!["x".into()],
                body: Term::Var { name: "x".into() },
                doc: None,
                suppress: vec![],
            })],
        };
        round_trip(m, "forall_with_constraint");
    }

    #[test]
    fn print_then_parse_round_trip_minimal_instance() {
        let m = Module {
            schema: ailang_core::SCHEMA.to_string(),
            name: "M".into(),
            imports: vec![],
            defs: vec![Def::Instance(InstanceDef {
                class: "Foo".into(),
                type_: Type::int(),
                methods: vec![InstanceMethod {
                    name: "m".into(),
                    body: Term::Lit { lit: Literal::Int { value: 5 } },
                }],
                doc: None,
            })],
        };
        round_trip(m, "minimal_instance");
    }

    /// Iter 22-floats.2 RED: `lex(print(L)) == L` round-trip property
    /// for Float literals. Six representative bit patterns:
    /// `1.5`, `0.0`, `-0.0`, `10.0`, `-0.375`, `1e10`. The round-trip
    /// uses the existing `round_trip(Module, &str)` helper, which
    /// prints the module to surface form, re-parses it, and asserts
    /// canonical bytes match. The Float arm in surface print MUST emit
    /// at least one of `.` or `e`/`E` so the lexer recognises the
    /// output as a Float (not an Int) — `f64::to_string` returns "1"
    /// for `1.0_f64`, "10000000000" for `1e10_f64`, and the printer's
    /// post-pass adds `.0` in those cases.
    #[test]
    fn print_then_parse_round_trip_float_literal() {
        use ailang_core::ast::*;
        for &bits in &[
            0x3ff8_0000_0000_0000u64, // 1.5
            0x0000_0000_0000_0000u64, // 0.0
            0x8000_0000_0000_0000u64, // -0.0
            0x4024_0000_0000_0000u64, // 10.0
            0xbfd8_0000_0000_0000u64, // -0.375
            0x4202_a05f_2000_0000u64, // 1e10
        ] {
            let m = Module {
                schema: ailang_core::SCHEMA.to_string(),
                name: "M".into(),
                imports: vec![],
                defs: vec![Def::Const(ConstDef {
                    name: "k".into(),
                    ty: Type::float(),
                    value: Term::Lit { lit: Literal::Float { bits } },
                    doc: None,
                })],
            };
            round_trip(m, &format!("float_literal_{bits:#018x}"));
        }
    }
}
