aver-lang 0.10.1

/// Aver → Dafny transpiler.
///
/// Generates a single `.dfy` file with:
/// - `datatype` declarations for sum types
/// - `datatype` wrappers for product types (records)
/// - `function` definitions for pure functions
/// - `lemma` stubs for verify-law blocks
/// - `assert` examples for verify-cases blocks
mod expr;
mod toplevel;

use crate::ast::{TopLevel, VerifyKind};
use crate::codegen::{CodegenContext, ProjectOutput};

/// Check if a function body uses the `?` (ErrorProp) operator.
/// Such functions require early-return semantics that Dafny pure functions cannot express.
fn body_uses_error_prop(body: &std::sync::Arc<crate::ast::FnBody>) -> bool {
    match body.as_ref() {
        crate::ast::FnBody::Block(stmts) => stmts.iter().any(|s| match s {
            crate::ast::Stmt::Binding(_, _, expr) => expr_uses_error_prop(expr),
            crate::ast::Stmt::Expr(expr) => expr_uses_error_prop(expr),
        }),
    }
}

fn expr_uses_error_prop(expr: &crate::ast::Spanned<crate::ast::Expr>) -> bool {
    use crate::ast::Expr;
    match &expr.node {
        Expr::ErrorProp(_) => true,
        Expr::FnCall(f, args) => expr_uses_error_prop(f) || args.iter().any(expr_uses_error_prop),
        Expr::BinOp(_, l, r) => expr_uses_error_prop(l) || expr_uses_error_prop(r),
        Expr::Match { subject, arms, .. } => {
            expr_uses_error_prop(subject) || arms.iter().any(|a| expr_uses_error_prop(&a.body))
        }
        Expr::Constructor(_, Some(arg)) => expr_uses_error_prop(arg),
        Expr::List(elems) | Expr::Tuple(elems) => elems.iter().any(expr_uses_error_prop),
        Expr::RecordCreate { fields, .. } => fields.iter().any(|(_, e)| expr_uses_error_prop(e)),
        Expr::RecordUpdate { base, updates, .. } => {
            expr_uses_error_prop(base) || updates.iter().any(|(_, e)| expr_uses_error_prop(e))
        }
        Expr::InterpolatedStr(parts) => parts.iter().any(|p| match p {
            crate::ast::StrPart::Parsed(e) => expr_uses_error_prop(e),
            _ => false,
        }),
        Expr::Attr(obj, _) => expr_uses_error_prop(obj),
        Expr::TailCall(inner) => inner.args.iter().any(expr_uses_error_prop),
        _ => false,
    }
}

/// Transpile an Aver program into a Dafny project.
pub fn transpile(ctx: &CodegenContext) -> ProjectOutput {
    let mut sections: Vec<String> = Vec::new();

    sections.push("// Generated by the Aver → Dafny transpiler".to_string());
    sections.push("// Pure core logic only (effectful functions are omitted)\n".to_string());

    // Prelude: Result/Option datatypes
    sections.push(DAFNY_PRELUDE.to_string());

    // Emit type definitions from dependent modules
    for module in &ctx.modules {
        for td in &module.type_defs {
            if let Some(code) = toplevel::emit_type_def(td) {
                sections.push(code);
            }
        }
    }

    // Emit type definitions from the main module
    for td in &ctx.type_defs {
        if let Some(code) = toplevel::emit_type_def(td) {
            sections.push(code);
        }
    }

    // Emit function definitions from dependent modules (pure only, no ? operator)
    for module in &ctx.modules {
        for fd in &module.fn_defs {
            if fd.effects.is_empty() && !body_uses_error_prop(&fd.body) {
                sections.push(toplevel::emit_fn_def(fd, ctx));
            }
        }
    }

    // Emit function definitions from the main module (pure only, no ? operator)
    for item in &ctx.items {
        if let TopLevel::FnDef(fd) = item
            && fd.effects.is_empty()
            && fd.name != "main"
            && !body_uses_error_prop(&fd.body)
        {
            sections.push(toplevel::emit_fn_def(fd, ctx));
        }
    }

    // Emit verify law blocks: sample assertions + universal lemma.
    let mut law_counter: std::collections::HashMap<String, usize> =
        std::collections::HashMap::new();
    for item in &ctx.items {
        if let TopLevel::Verify(vb) = item
            && let VerifyKind::Law(law) = &vb.kind
        {
            let count = law_counter.entry(vb.fn_name.clone()).or_insert(0);
            *count += 1;
            let suffix = if *count > 1 {
                format!("_{}", count)
            } else {
                String::new()
            };

            // 1. Sample assertions from the domain expansion (concrete smoke tests)
            if !vb.cases.is_empty()
                && let Some(code) = toplevel::emit_law_samples(vb, law, ctx, &suffix)
            {
                sections.push(code);
            }

            // 2. Universal lemma (when clause becomes requires)
            sections.push(toplevel::emit_verify_law(vb, law, ctx));
        }
    }

    let content = sections.join("\n");
    let file_name = format!("{}.dfy", ctx.project_name);

    ProjectOutput {
        files: vec![(file_name, content)],
    }
}

const DAFNY_PRELUDE: &str = r#"// --- Prelude: standard types and helpers ---

datatype Result<T, E> = Ok(value: T) | Err(error: E)

datatype Option<T> = None | Some(value: T)

function ResultWithDefault<T, E>(r: Result<T, E>, d: T): T {
  match r
  case Ok(v) => v
  case Err(_) => d
}

function OptionWithDefault<T>(o: Option<T>, d: T): T {
  match o
  case Some(v) => v
  case None => d
}

function OptionToResult<T, E>(o: Option<T>, err: E): Result<T, E> {
  match o
  case Some(v) => Result.Ok(v)
  case None => Result.Err(err)
}

function ListReverse<T>(xs: seq<T>): seq<T>
  decreases |xs|
{
  if |xs| == 0 then []
  else ListReverse(xs[1..]) + [xs[0]]
}

function ListHead<T>(xs: seq<T>): Option<T> {
  if |xs| == 0 then None
  else Some(xs[0])
}

function ListTail<T>(xs: seq<T>): seq<T> {
  if |xs| == 0 then []
  else xs[1..]
}

function ListTake<T>(xs: seq<T>, n: int): seq<T> {
  if n <= 0 then []
  else if n >= |xs| then xs
  else xs[..n]
}

function ListDrop<T>(xs: seq<T>, n: int): seq<T> {
  if n <= 0 then xs
  else if n >= |xs| then []
  else xs[n..]
}

function MapGet<K, V>(m: map<K, V>, k: K): Option<V> {
  if k in m then Some(m[k])
  else None
}

// --- String/Char helpers (opaque stubs for verification) ---

function IntToString(n: int): string
function IntFromString(s: string): Result<int, string>
function FloatToString(r: real): string
function FloatFromString(s: string): Result<real, string>
function StringCharAt(s: string, i: int): Option<string> {
  if 0 <= i < |s| then Option.Some([s[i]]) else Option.None
}
function StringChars(s: string): seq<string> {
  seq(|s|, (i: int) requires 0 <= i < |s| => [s[i]])
}
function StringJoin(sep: string, parts: seq<string>): string
  decreases |parts|
{
  if |parts| == 0 then ""
  else if |parts| == 1 then parts[0]
  else parts[0] + sep + StringJoin(sep, parts[1..])
}
function CharToCode(c: string): int
function CharFromCode(n: int): Option<string>
function MapEntries<K, V>(m: map<K, V>): seq<(K, V)>
function MapFromList<K, V>(entries: seq<(K, V)>): map<K, V>
  decreases |entries|
{
  if |entries| == 0 then map[]
  else MapFromList(entries[..|entries|-1])[entries[|entries|-1].0 := entries[|entries|-1].1]
}
function ByteToHex(b: int): Result<string, string>
function ByteFromHex(s: string): Result<int, string>
function ToString<T>(v: T): string
"#;