Add experimental Dafny backend

src/dafny/ast.rs

@@ -0,0 +1,225 @@
+/// A full Dafny file emitted by the backend.
+#[derive(Clone, Debug, PartialEq, Eq)]
+pub struct File {
+    pub decls: Vec<Decl>,
+}
+
+/// Top-level Dafny declarations supported by the current backend.
+#[derive(Clone, Debug, PartialEq, Eq)]
+pub enum Decl {
+    Type(TypeDecl),
+    Function(FunctionDecl),
+    Method(MethodDecl),
+}
+
+/// A lightweight Dafny `type` declaration for an abstract HeyVL domain.
+#[derive(Clone, Debug, PartialEq, Eq)]
+pub struct TypeDecl {
+    pub name: String,
+}
+
+/// A Dafny `function` declaration, optionally with a definition body.
+#[derive(Clone, Debug, PartialEq, Eq)]
+pub struct FunctionDecl {
+    pub name: String,
+    pub params: Vec<Param>,
+    pub return_ty: Type,
+    pub body: Option<Expr>,
+}
+
+/// A Dafny `method` declaration with contracts and an optional body.
+#[derive(Clone, Debug, PartialEq, Eq)]
+pub struct MethodDecl {
+    pub axiom: bool,
+    pub name: String,
+    pub params: Vec<Param>,
+    pub returns: Vec<Param>,
+    pub requires: Vec<Expr>,
+    pub ensures: Vec<Expr>,
+    pub decreases_star: bool,
+    pub body: Option<Block>,
+}
+
+/// A sequence of Dafny statements surrounded by `{ ... }`.
+#[derive(Clone, Debug, PartialEq, Eq)]
+pub struct Block {
+    pub stmts: Vec<Stmt>,
+}
+
+/// The statement fragment the backend knows how to emit.
+#[derive(Clone, Debug, PartialEq, Eq)]
+pub enum Stmt {
+    Block(Block),
+    Var(VarDecl),
+    Assign(AssignStmt),
+    Call(CallStmt),
+    AssignCall(AssignCallStmt),
+    SuchThatAssign(SuchThatAssignStmt),
+    Assert(AssertStmt),
+    Assume(AssumeStmt),
+    If(IfStmt),
+    While(WhileStmt),
+}
+
+/// A Dafny local variable declaration.
+#[derive(Clone, Debug, PartialEq, Eq)]
+pub struct VarDecl {
+    pub name: String,
+    pub ty: Type,
+    pub init: VarInit,
+}
+
+/// The initialization forms used for local variables in emitted Dafny.
+#[derive(Clone, Debug, PartialEq, Eq)]
+pub enum VarInit {
+    Expr(Expr),
+    MethodCall { method: String, args: Vec<Expr> },
+    SuchThat(Expr),
+}
+
+#[derive(Clone, Debug, PartialEq, Eq)]
+pub struct AssignStmt {
+    pub lhs: String,
+    pub rhs: Expr,
+}
+
+#[derive(Clone, Debug, PartialEq, Eq)]
+pub struct CallStmt {
+    pub method: String,
+    pub args: Vec<Expr>,
+}
+
+#[derive(Clone, Debug, PartialEq, Eq)]
+pub struct AssignCallStmt {
+    pub lhs: Vec<String>,
+    pub method: String,
+    pub args: Vec<Expr>,
+}
+
+#[derive(Clone, Debug, PartialEq, Eq)]
+pub struct SuchThatAssignStmt {
+    pub lhs: Vec<String>,
+    pub predicate: Expr,
+}
+
+#[derive(Clone, Debug, PartialEq, Eq)]
+pub struct AssertStmt {
+    pub expr: Expr,
+}
+
+#[derive(Clone, Debug, PartialEq, Eq)]
+pub struct AssumeStmt {
+    pub axiom: bool,
+    pub expr: Expr,
+}
+
+#[derive(Clone, Debug, PartialEq, Eq)]
+pub struct IfStmt {
+    pub cond: Expr,
+    pub then_branch: Block,
+    pub else_branch: Block,
+}
+
+#[derive(Clone, Debug, PartialEq, Eq)]
+pub struct WhileStmt {
+    pub cond: Expr,
+    pub invariants: Vec<Expr>,
+    pub decreases_star: bool,
+    pub body: Block,
+}
+
+#[derive(Clone, Debug, PartialEq, Eq)]
+pub struct Param {
+    pub name: String,
+    pub ty: Type,
+}
+
+/// The minimal Dafny type fragment needed by the backend.
+#[derive(Clone, Debug, PartialEq, Eq)]
+pub enum Type {
+    Bool,
+    Int,
+    Nat,
+    Seq(Box<Type>),
+    Named(String),
+}
+
+/// The expression fragment shared by the lowering and pretty-printing passes.
+#[derive(Clone, Debug, PartialEq, Eq)]
+pub enum Expr {
+    Var(String),
+    BoolLit(bool),
+    NumberLit(String),
+    StringLit(String),
+    Call {
+        function: String,
+        args: Vec<Expr>,
+    },
+    Ite {
+        cond: Box<Expr>,
+        then_expr: Box<Expr>,
+        else_expr: Box<Expr>,
+    },
+    Binary {
+        op: BinaryOp,
+        lhs: Box<Expr>,
+        rhs: Box<Expr>,
+    },
+    Unary {
+        op: UnaryOp,
+        expr: Box<Expr>,
+    },
+    Quantified {
+        quantifier: Quantifier,
+        vars: Vec<QuantVar>,
+        triggers: Vec<Vec<Expr>>,
+        body: Box<Expr>,
+    },
+    SeqLen(Box<Expr>),
+    Index {
+        collection: Box<Expr>,
+        index: Box<Expr>,
+    },
+    Update {
+        collection: Box<Expr>,
+        index: Box<Expr>,
+        value: Box<Expr>,
+    },
+}
+
+#[derive(Clone, Debug, PartialEq, Eq)]
+pub enum BinaryOp {
+    Add,
+    Sub,
+    Mul,
+    Div,
+    Mod,
+    And,
+    Or,
+    Eq,
+    Lt,
+    Le,
+    Ne,
+    Ge,
+    Gt,
+    Impl,
+}
+
+#[derive(Clone, Debug, PartialEq, Eq)]
+pub enum UnaryOp {
+    Not,
+    Parens,
+}
+
+#[derive(Clone, Debug, PartialEq, Eq)]
+pub enum Quantifier {
+    Forall,
+    Exists,
+}
+
+/// A typed quantified variable in a Dafny quantifier.
+#[derive(Clone, Debug, PartialEq, Eq)]
+pub struct QuantVar {
+    pub name: String,
+    pub ty: Type,
+}

src/dafny/index.rs

@@ -0,0 +1,152 @@
+use regex::Regex;
+
+use crate::{
+    ast::{
+        AxiomDecl, DeclKind, DeclRef, DomainDecl, DomainSpec, FileId, FuncDecl, Ident, ProcDecl,
+    },
+    driver::{
+        front::{Module, SourceUnit},
+        item::SourceUnitName,
+    },
+};
+
+/// A flattened reference to one declaration that may appear in an emitted file.
+#[derive(Clone)]
+pub(crate) enum FlatDeclRef {
+    Proc(DeclRef<ProcDecl>),
+    Domain(DeclRef<DomainDecl>),
+    Func(DeclRef<FuncDecl>),
+    Axiom(DeclRef<AxiomDecl>),
+}
+
+#[derive(Clone, Copy, PartialEq, Eq)]
+pub(crate) enum FlatDeclKind {
+    Proc,
+    Domain,
+    Func,
+    Axiom,
+}
+
+/// Metadata used to group and order declarations during file emission.
+#[derive(Clone)]
+pub(crate) struct FlatDeclRecord {
+    pub(crate) ident: Ident,
+    pub(crate) file_id: FileId,
+    pub(crate) kind: FlatDeclKind,
+    pub(crate) decl: FlatDeclRef,
+    pub(crate) source_name: Option<SourceUnitName>,
+}
+
+/// Lookup table from identifiers to the flattened declaration order used by the backend.
+pub(crate) struct DeclIndex {
+    pub(crate) ordered: Vec<FlatDeclRecord>,
+    by_ident: std::collections::HashMap<Ident, usize>,
+}
+
+impl DeclIndex {
+    /// Collect top-level and domain-nested declarations into a single stable order.
+    pub(crate) fn new(module: &Module) -> Self {
+        let mut ordered = Vec::new();
+        let mut by_ident = std::collections::HashMap::new();
+
+        for item in &module.items {
+            match &**item {
+                SourceUnit::Decl(DeclKind::ProcDecl(proc_ref)) => {
+                    let record = FlatDeclRecord {
+                        ident: proc_ref.borrow().name,
+                        file_id: proc_ref.borrow().span.file,
+                        kind: FlatDeclKind::Proc,
+                        decl: FlatDeclRef::Proc(proc_ref.clone()),
+                        source_name: Some(item.name().clone()),
+                    };
+                    by_ident.insert(record.ident, ordered.len());
+                    ordered.push(record);
+                }
+                SourceUnit::Decl(DeclKind::DomainDecl(domain_ref)) => {
+                    let domain = domain_ref.borrow();
+                    let file_id = domain.span.file;
+                    let record = FlatDeclRecord {
+                        ident: domain.name,
+                        file_id,
+                        kind: FlatDeclKind::Domain,
+                        decl: FlatDeclRef::Domain(domain_ref.clone()),
+                        source_name: None,
+                    };
+                    by_ident.insert(record.ident, ordered.len());
+                    ordered.push(record);
+
+                    for spec in &domain.body {
+                        let record = match spec {
+                            DomainSpec::Function(func_ref) => FlatDeclRecord {
+                                ident: func_ref.borrow().name,
+                                file_id,
+                                kind: FlatDeclKind::Func,
+                                decl: FlatDeclRef::Func(func_ref.clone()),
+                                source_name: None,
+                            },
+                            DomainSpec::Axiom(axiom_ref) => FlatDeclRecord {
+                                ident: axiom_ref.borrow().name,
+                                file_id,
+                                kind: FlatDeclKind::Axiom,
+                                decl: FlatDeclRef::Axiom(axiom_ref.clone()),
+                                source_name: None,
+                            },
+                        };
+                        by_ident.insert(record.ident, ordered.len());
+                        ordered.push(record);
+                    }
+                }
+                SourceUnit::Decl(DeclKind::FuncDecl(func_ref)) => {
+                    let record = FlatDeclRecord {
+                        ident: func_ref.borrow().name,
+                        file_id: func_ref.borrow().span.file,
+                        kind: FlatDeclKind::Func,
+                        decl: FlatDeclRef::Func(func_ref.clone()),
+                        source_name: None,
+                    };
+                    by_ident.insert(record.ident, ordered.len());
+                    ordered.push(record);
+                }
+                SourceUnit::Decl(DeclKind::AxiomDecl(axiom_ref)) => {
+                    let record = FlatDeclRecord {
+                        ident: axiom_ref.borrow().name,
+                        file_id: axiom_ref.borrow().span.file,
+                        kind: FlatDeclKind::Axiom,
+                        decl: FlatDeclRef::Axiom(axiom_ref.clone()),
+                        source_name: None,
+                    };
+                    by_ident.insert(record.ident, ordered.len());
+                    ordered.push(record);
+                }
+                SourceUnit::Decl(_) | SourceUnit::Raw(_) => {}
+            }
+        }
+
+        DeclIndex { ordered, by_ident }
+    }
+
+    pub(crate) fn get(&self, ident: Ident) -> Option<&FlatDeclRecord> {
+        self.by_ident.get(&ident).map(|index| &self.ordered[*index])
+    }
+
+    /// Return the selected top-level `proc` roots defined in one source file.
+    pub(crate) fn selected_roots_for_file(
+        &self,
+        file_id: FileId,
+        filter: Option<&Regex>,
+    ) -> Vec<Ident> {
+        self.ordered
+            .iter()
+            .filter(|record| {
+                record.kind == FlatDeclKind::Proc
+                    && record.file_id == file_id
+                    && record
+                        .source_name
+                        .as_ref()
+                        .map(|name| filter.is_none_or(|regex| regex.is_match(&name.to_string())))
+                        .unwrap_or(false)
+            })
+            .map(|record| record.ident)
+            .collect()
+    }
+}