assura 0.4.0

use super::*;

// `assura diff` -- structural diff between contract files
// ---------------------------------------------------------------------------

pub(crate) fn extract_decl_summary(
    sf: &SourceFile,
) -> std::collections::BTreeMap<String, Vec<String>> {
    let mut result = std::collections::BTreeMap::new();
    for spanned_decl in &sf.decls {
        let decl = &spanned_decl.node;
        let name = decl
            .name()
            .map(|s| s.to_string())
            .unwrap_or_else(|| "<anon>".to_string());
        let clauses: Vec<String> = decl
            .clauses()
            .iter()
            .map(|cl| format!("{:?}: {}", cl.kind, format_clause_body(cl)))
            .collect();
        result.insert(name, clauses);
    }
    result
}

/// Human-readable clause body (Assura surface syntax), not Debug.
pub(crate) fn format_clause_body(clause: &assura_parser::ast::Clause) -> String {
    assura_parser::display::expr_to_string(&clause.body)
}

fn validate_diff_format(format: &str, as_json: bool) {
    crate::validate_human_json_format(format, "diff", as_json);
}

/// Structural diff result. When `emit` is false, JSON is not printed (used so
/// `--verify --json` can emit a single combined document).
pub(crate) fn run_diff(
    old_path: &str,
    new_path: &str,
    format: &str,
    as_json: bool,
) -> (bool, serde_json::Value) {
    validate_diff_format(format, as_json);
    let is_json = format == "json";
    let old_src = match fs::read_to_string(old_path) {
        Ok(s) => s,
        Err(e) => {
            if is_json {
                let report = serde_json::json!({
                    "ok": false,
                    "error": "cannot_read",
                    "path": old_path,
                    "message": format!("Error reading {old_path}: {e}"),
                });
                println!("{}", serde_json::to_string_pretty(&report).unwrap());
            } else {
                eprintln!("Error reading {old_path}: {e}");
            }
            process::exit(1);
        }
    };
    let new_src = match fs::read_to_string(new_path) {
        Ok(s) => s,
        Err(e) => {
            if is_json {
                let report = serde_json::json!({
                    "ok": false,
                    "error": "cannot_read",
                    "path": new_path,
                    "message": format!("Error reading {new_path}: {e}"),
                });
                println!("{}", serde_json::to_string_pretty(&report).unwrap());
            } else {
                eprintln!("Error reading {new_path}: {e}");
            }
            process::exit(1);
        }
    };

    let (old_ast, old_errs) = assura_parser::parse(&old_src);
    let (new_ast, new_errs) = assura_parser::parse(&new_src);

    if !old_errs.is_empty() && !is_json {
        eprintln!("Warning: {old_path} has {} parse error(s)", old_errs.len());
    }
    if !new_errs.is_empty() && !is_json {
        eprintln!("Warning: {new_path} has {} parse error(s)", new_errs.len());
    }

    let old_decls = old_ast
        .as_ref()
        .map(extract_decl_summary)
        .unwrap_or_default();
    let new_decls = new_ast
        .as_ref()
        .map(extract_decl_summary)
        .unwrap_or_default();

    let mut changes = Vec::new();
    let mut has_diff = false;

    for (name, old_clauses) in &old_decls {
        if !new_decls.contains_key(name) {
            has_diff = true;
            changes.push(DiffEntry {
                name: name.clone(),
                kind: "removed".to_string(),
                added_clauses: Vec::new(),
                removed_clauses: old_clauses.clone(),
                unchanged_clauses: Vec::new(),
            });
        }
    }

    for (name, new_clauses) in &new_decls {
        match old_decls.get(name) {
            None => {
                has_diff = true;
                changes.push(DiffEntry {
                    name: name.clone(),
                    kind: "added".to_string(),
                    added_clauses: new_clauses.clone(),
                    removed_clauses: Vec::new(),
                    unchanged_clauses: Vec::new(),
                });
            }
            Some(old_clauses) => {
                let added: Vec<String> = new_clauses
                    .iter()
                    .filter(|c| !old_clauses.contains(c))
                    .cloned()
                    .collect();
                let removed: Vec<String> = old_clauses
                    .iter()
                    .filter(|c| !new_clauses.contains(c))
                    .cloned()
                    .collect();
                let unchanged: Vec<String> = new_clauses
                    .iter()
                    .filter(|c| old_clauses.contains(c))
                    .cloned()
                    .collect();
                if !added.is_empty() || !removed.is_empty() {
                    has_diff = true;
                    changes.push(DiffEntry {
                        name: name.clone(),
                        kind: "modified".to_string(),
                        added_clauses: added,
                        removed_clauses: removed,
                        unchanged_clauses: unchanged,
                    });
                }
            }
        }
    }

    let json = serde_json::json!({
        "identical": !has_diff,
        "changes": changes.iter().map(|c| serde_json::json!({
            "name": c.name,
            "kind": c.kind,
            "added_clauses": c.added_clauses,
            "removed_clauses": c.removed_clauses,
            "unchanged_clauses": c.unchanged_clauses,
        })).collect::<Vec<_>>(),
    });

    if format == "json" {
        // Caller may suppress print when combining with --verify.
        // Default path prints here only when used alone; cli.rs decides.
    } else {
        if !has_diff {
            println!("No structural differences.");
        }
        for entry in &changes {
            match entry.kind.as_str() {
                "added" => println!("{}:  (new)", entry.name),
                "removed" => println!("{}:  (removed)", entry.name),
                _ => println!("{}:", entry.name),
            }
            for c in &entry.removed_clauses {
                println!("  - {c}");
            }
            for c in &entry.added_clauses {
                println!("  + {c}");
            }
            for c in &entry.unchanged_clauses {
                println!("    {c}");
            }
            println!();
        }
    }

    (has_diff, json)
}

/// Structured evolution result for JSON (no Debug dumps).
fn evolution_check_json(r: &assura_smt::VerificationResult) -> serde_json::Value {
    r.to_json_value()
}

fn evolution_is_ok(r: &assura_smt::VerificationResult) -> bool {
    matches!(r, assura_smt::VerificationResult::Verified { .. })
}

/// Run SMT-based evolution verification on two contract files.
///
/// Parses both files and checks backward compatibility:
/// - Precondition weakening: old_requires => new_requires
/// - Postcondition strengthening: new_ensures => old_ensures
///
/// When `structural` is `Some`, JSON mode emits a **single** document that
/// includes both the structural diff and evolution results (avoids two JSON
/// objects on stdout that break `json.loads`).
pub(crate) fn run_diff_verify(
    old_path: &str,
    new_path: &str,
    format: &str,
    structural: Option<serde_json::Value>,
    as_json: bool,
) {
    validate_diff_format(format, as_json);
    let is_json = format == "json";
    let old_src = match fs::read_to_string(old_path) {
        Ok(s) => s,
        Err(e) => {
            if is_json {
                let report = serde_json::json!({
                    "ok": false,
                    "error": "cannot_read",
                    "path": old_path,
                    "message": format!("Error reading {old_path}: {e}"),
                });
                println!("{}", serde_json::to_string_pretty(&report).unwrap());
            } else {
                eprintln!("Error reading {old_path}: {e}");
            }
            process::exit(1);
        }
    };
    let new_src = match fs::read_to_string(new_path) {
        Ok(s) => s,
        Err(e) => {
            if is_json {
                let report = serde_json::json!({
                    "ok": false,
                    "error": "cannot_read",
                    "path": new_path,
                    "message": format!("Error reading {new_path}: {e}"),
                });
                println!("{}", serde_json::to_string_pretty(&report).unwrap());
            } else {
                eprintln!("Error reading {new_path}: {e}");
            }
            process::exit(1);
        }
    };

    let (old_ast, old_errs) = assura_parser::parse(&old_src);
    let (new_ast, new_errs) = assura_parser::parse(&new_src);

    if !old_errs.is_empty() || old_ast.is_none() {
        eprintln!("Cannot verify evolution: {old_path} has parse errors");
        process::exit(1);
    }
    if !new_errs.is_empty() || new_ast.is_none() {
        eprintln!("Cannot verify evolution: {new_path} has parse errors");
        process::exit(1);
    }

    let old_ast = old_ast.unwrap();
    let new_ast = new_ast.unwrap();

    let results = assura_smt::verify_file_evolution(&old_ast, &new_ast);

    if results.is_empty() {
        if format == "json" {
            let mut doc = serde_json::json!({
                "evolution": [],
                "compatible": true,
            });
            if let Some(s) = structural {
                doc["identical"] = s
                    .get("identical")
                    .cloned()
                    .unwrap_or(serde_json::json!(true));
                doc["changes"] = s
                    .get("changes")
                    .cloned()
                    .unwrap_or_else(|| serde_json::json!([]));
            }
            println!("{}", serde_json::to_string_pretty(&doc).unwrap());
        } else {
            println!("No matching contracts to verify evolution.");
        }
        return;
    }

    let mut all_pass = true;
    if format == "json" {
        let json_results: Vec<serde_json::Value> = results
            .iter()
            .map(|r| {
                let pre_ok = evolution_is_ok(&r.precondition_weakening);
                let post_ok = evolution_is_ok(&r.postcondition_strengthening);
                if !pre_ok || !post_ok {
                    all_pass = false;
                }
                serde_json::json!({
                    "contract": r.contract_name,
                    "precondition_weakening": evolution_check_json(&r.precondition_weakening),
                    "postcondition_strengthening": evolution_check_json(&r.postcondition_strengthening),
                    "compatible": pre_ok && post_ok,
                })
            })
            .collect();
        let mut doc = serde_json::json!({
            "evolution": json_results,
            "compatible": all_pass,
        });
        if let Some(s) = structural {
            doc["identical"] = s
                .get("identical")
                .cloned()
                .unwrap_or(serde_json::json!(false));
            doc["changes"] = s
                .get("changes")
                .cloned()
                .unwrap_or_else(|| serde_json::json!([]));
        }
        println!("{}", serde_json::to_string_pretty(&doc).unwrap());
    } else {
        println!("\nContract evolution verification:");
        for r in &results {
            println!("  {}:", r.contract_name);
            let pre_status = match &r.precondition_weakening {
                assura_smt::VerificationResult::Verified { .. } => "verified",
                assura_smt::VerificationResult::Counterexample { .. } => {
                    all_pass = false;
                    "FAILED (preconditions strengthened)"
                }
                assura_smt::VerificationResult::Unknown { reason, .. } => {
                    eprintln!("    warning: {reason}");
                    "unknown"
                }
                assura_smt::VerificationResult::Timeout { .. } => {
                    all_pass = false;
                    "timeout"
                }
            };
            println!("    precondition weakening  ... {pre_status}");

            let post_status = match &r.postcondition_strengthening {
                assura_smt::VerificationResult::Verified { .. } => "verified",
                assura_smt::VerificationResult::Counterexample { .. } => {
                    all_pass = false;
                    "FAILED (postconditions weakened)"
                }
                assura_smt::VerificationResult::Unknown { reason, .. } => {
                    eprintln!("    warning: {reason}");
                    "unknown"
                }
                assura_smt::VerificationResult::Timeout { .. } => {
                    all_pass = false;
                    "timeout"
                }
            };
            println!("    postcondition strength. ... {post_status}");
        }
    }

    if !all_pass {
        process::exit(1);
    }
}

pub(crate) struct DiffEntry {
    name: String,
    kind: String,
    added_clauses: Vec<String>,
    removed_clauses: Vec<String>,
    unchanged_clauses: Vec<String>,
}

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

    #[test]
    fn format_clause_body_is_surface_syntax_not_debug() {
        let src = r#"
contract C {
  input(x: Int)
  ensures { x >= 0 }
}
"#;
        let (ast, errs) = assura_parser::parse(src);
        assert!(errs.is_empty(), "{errs:?}");
        let sf = ast.expect("ast");
        let summary = extract_decl_summary(&sf);
        let clauses = summary.get("C").expect("contract C");
        let ensures = clauses
            .iter()
            .find(|c| c.starts_with("Ensures:"))
            .expect("ensures clause");
        // Must not dump Debug(Spanned { node: ... })
        assert!(
            !ensures.contains("Spanned"),
            "diff body must not use Debug format: {ensures}"
        );
        assert!(
            ensures.contains("x") && ensures.contains("0"),
            "expected surface expression, got {ensures}"
        );
        // Prefer readable comparison operator
        assert!(
            ensures.contains(">=") || ensures.contains("≥"),
            "expected comparison in body: {ensures}"
        );
    }
}

// ===========================================================================
// Integration tests: full pipeline from source text through all passes
// ===========================================================================