use crate::ast::display::{
format_ast_type as format_type, format_const_value as format_const_expr,
};
use crate::ast::{File, FnDef, Item, Param, Type};
pub fn generate_scaffold(file: &File) -> String {
let mut out = String::new();
let kind = match file.kind {
crate::ast::FileKind::Program => "program",
crate::ast::FileKind::Module => "module",
};
out.push_str(&format!("{} {}\n", kind, file.name.node));
for u in &file.uses {
out.push_str(&format!("\nuse {}", u.node));
}
for item in &file.items {
out.push('\n');
match &item.node {
Item::Fn(func) => {
out.push_str(&scaffold_function(func));
}
Item::Const(c) => {
if c.is_pub {
out.push_str("pub ");
}
out.push_str(&format!(
"const {}: {} = {}\n",
c.name.node,
format_type(&c.ty.node),
format_const_expr(&c.value.node),
));
}
Item::Struct(s) => {
if s.is_pub {
out.push_str("pub ");
}
out.push_str(&format!("struct {} {{\n", s.name.node));
for field in &s.fields {
if field.is_pub {
out.push_str(" pub ");
} else {
out.push_str(" ");
}
out.push_str(&format!(
"{}: {},\n",
field.name.node,
format_type(&field.ty.node),
));
}
out.push_str("}\n");
}
Item::Event(e) => {
out.push_str(&format!("event {} {{\n", e.name.node));
for field in &e.fields {
out.push_str(&format!(
" {}: {},\n",
field.name.node,
format_type(&field.ty.node),
));
}
out.push_str("}\n");
}
}
}
out
}
fn scaffold_function(func: &FnDef) -> String {
let mut out = String::new();
let requires: Vec<&str> = func.requires.iter().map(|s| s.node.as_str()).collect();
let ensures: Vec<&str> = func.ensures.iter().map(|s| s.node.as_str()).collect();
for r in &requires {
out.push_str(&format!("#[requires({})]\n", r));
}
for e in &ensures {
out.push_str(&format!("#[ensures({})]\n", e));
}
if func.is_pub {
out.push_str("pub ");
}
if func.is_test {
out.push_str("#[test]\n");
}
out.push_str(&format!("fn {}", func.name.node));
if !func.type_params.is_empty() {
let tp: Vec<&str> = func.type_params.iter().map(|p| p.node.as_str()).collect();
out.push_str(&format!("<{}>", tp.join(", ")));
}
out.push('(');
let params: Vec<String> = func
.params
.iter()
.map(|p| format!("{}: {}", p.name.node, format_type(&p.ty.node)))
.collect();
out.push_str(¶ms.join(", "));
out.push(')');
if let Some(ref ret) = func.return_ty {
out.push_str(&format!(" -> {}", format_type(&ret.node)));
}
out.push_str(" {\n");
let has_specs = !requires.is_empty() || !ensures.is_empty();
if has_specs {
out.push_str(&spec_comment(&requires, &ensures));
out.push('\n');
}
let fn_name = &func.name.node;
if let Some(ref ret_ty) = func.return_ty {
out.push_str(&format!(" // TODO: Implement {} logic\n", fn_name));
if !ensures.is_empty() {
out.push_str(&format!(
" // The result must satisfy: {}\n",
ensures.join(", "),
));
}
let result_expr = synthesise_result_expr(&ensures, &func.params, &ret_ty.node);
out.push_str(&format!(
" let result: {} = {}\n",
format_type(&ret_ty.node),
result_expr,
));
for e in &ensures {
let assertion = ensures_to_assertion(e, &ret_ty.node);
out.push_str(&format!(
"\n // Verify postcondition\n {}\n",
assertion
));
}
out.push_str("\n result\n");
} else {
out.push_str(&format!(" // TODO: Implement {} logic\n", fn_name));
for r in &requires {
out.push_str(&format!(" assert({})\n", r));
}
for e in &ensures {
if *e != "true" {
out.push_str(&format!(" assert({})\n", e));
}
}
}
out.push_str("}\n");
out
}
fn spec_comment(requires: &[&str], ensures: &[&str]) -> String {
let mut out = String::new();
out.push_str(" // Specification:\n");
for r in requires {
out.push_str(&format!(" // requires: {}\n", r));
}
for e in ensures {
out.push_str(&format!(" // ensures: {}\n", e));
}
out
}
pub fn default_value(ty: &Type) -> String {
match ty {
Type::Field | Type::XField | Type::U32 => "0".to_string(),
Type::Bool => "false".to_string(),
Type::Digest => "0".to_string(),
Type::Array(inner, size) => {
let elem = default_value(inner);
if let Some(n) = size.as_literal() {
let elems: Vec<String> = (0..n).map(|_| elem.clone()).collect();
format!("[{}]", elems.join(", "))
} else {
format!("[{}; {}]", elem, size)
}
}
Type::Tuple(elems) => {
let parts: Vec<String> = elems.iter().map(default_value).collect();
format!("({})", parts.join(", "))
}
Type::Named(_) => "0".to_string(),
}
}
pub fn extract_variables(spec: &str) -> Vec<String> {
let keywords: &[&str] = &[
"true", "false", "old", "result", "let", "if", "else", "for", "fn", "return",
];
let mut vars = Vec::new();
let mut seen = std::collections::BTreeSet::new();
let mut chars = spec.char_indices().peekable();
while let Some(&(i, c)) = chars.peek() {
if c.is_ascii_alphabetic() || c == '_' {
let start = i;
while let Some(&(_, nc)) = chars.peek() {
if nc.is_ascii_alphanumeric() || nc == '_' {
chars.next();
} else {
break;
}
}
let end = chars.peek().map(|&(idx, _)| idx).unwrap_or(spec.len());
let word = &spec[start..end];
if !keywords.contains(&word) && !seen.contains(word) {
seen.insert(word.to_string());
vars.push(word.to_string());
}
} else {
chars.next();
}
}
vars
}
fn synthesise_result_expr(ensures: &[&str], params: &[Param], ret_ty: &Type) -> String {
for clause in ensures {
if let Some(expr) = try_extract_result_expr(clause, params) {
return expr;
}
}
default_value(ret_ty)
}
fn try_extract_result_expr(clause: &str, params: &[Param]) -> Option<String> {
let param_names: Vec<&str> = params.iter().map(|p| p.name.node.as_str()).collect();
if let Some(rhs) = clause
.strip_prefix("result == ")
.or_else(|| clause.strip_prefix("result =="))
{
let rhs = rhs.trim();
if !rhs.is_empty() {
return Some(rhs.to_string());
}
}
if let Some(eq_pos) = clause.find(" == ") {
let lhs = clause[..eq_pos].trim();
let rhs = clause[eq_pos + 4..].trim();
if is_simple_ident(lhs) && !param_names.contains(&lhs) && !rhs.is_empty() {
return Some(rhs.to_string());
}
}
None
}
fn is_simple_ident(s: &str) -> bool {
let mut chars = s.chars();
match chars.next() {
Some(c) if c.is_ascii_alphabetic() || c == '_' => {}
_ => return false,
}
chars.all(|c| c.is_ascii_alphanumeric() || c == '_')
}
fn ensures_to_assertion(clause: &str, _ret_ty: &Type) -> String {
if clause.contains("result") {
return format!("assert({})", clause);
}
if let Some(eq_pos) = clause.find(" == ") {
let lhs = clause[..eq_pos].trim();
let rhs = clause[eq_pos + 4..].trim();
if is_simple_ident(lhs) {
return format!("assert(result == {})", rhs);
}
}
format!("assert({})", clause)
}
#[cfg(test)]
mod tests;