dafny-lang / dafny

Dafny is a verification-aware programming language
https://dafny.org
Other
2.94k stars 263 forks source link

Dafny-to-Rust code generation is not simplifying all paths #5755

Closed MikaelMayer closed 2 months ago

MikaelMayer commented 2 months ago

Currently, the Dafny-to-Rust code generation has the nice feature that it adds "use" clauses to simplify some paths. However, this simplification currently happens only at the top-level of types, not in expressions. For example, the following generated Rust AST

pub mod Test {
  fn DoSomething(i: ::dafny_runtime::DafnyInt) {
    let mut n: ::dafny_runtime::DafnyInt = i;
  }
}

is currently rewritten to

pub mod Test {
  use dafny_runtime::DafnyInt;
  fn DoSomething(i: DafnyInt) {
    let mut n: ::dafny_runtime::DafnyInt = i;
  }
}

Note the simplification in the type parameters, but not in the body of the function.