search

epfl-lara / rust-stainless

An experimental Rust frontend for Stainless
Apache License 2.0
6 stars 2 forks source link

Add immutable Stainless Map #127

Closed yannbolliger closed 3 years ago

yannbolliger commented 3 years ago

Closes #118. Depends on #128.

The implementation of the map follows exactly, the one in Scala: https://github.com/epfl-lara/stainless/blob/20d258dc159723eff875be8d50de98bf310c1a16/frontends/scalac/src/main/scala/stainless/frontends/scalac/CodeExtraction.scala#L1190-L1213

To be able to usestd::option::Option as internal type in the map, we sometimes have to first extract it, and the be able to synthetise it (and its variants). This is currently done, in the std_items module, however, will have to be revisited, once other (non-std) things need to be synthetised. The only downside of the current implementation is that all the synthesising methods polute the method namespace of the BaseExtractor (you always have self.std_option_type() available):

  pub(super) fn std_option_type(&mut self, tpe: st::Type<'l>) -> st::Type<'l> {
  pub(super) fn std_option_none(&mut self, tpe: st::Type<'l>) -> st::Expr<'l> {
  pub(super) fn std_option_some(&mut self, val: st::Expr<'l>, tpe: st::Type<'l>) -> st::Expr<'l> {
  pub(super) fn std_option_some_type(&mut self, tpe: st::Type<'l>) -> st::Type<'l> {
  pub(super) fn std_option_some_value(&mut self, some: st::Expr<'l>) -> st::Expr<'l> {

Some scoping would be more readable: self.synth.std_option_type().

There is no backing runtime implementation for the map yet, this is tracked in #117.