Add old helper.

epfl-lara · Jul 21, 2021 · 67e4839 · 67e4839
1 parent fd85321
commit 67e4839
Show file tree

Hide file tree

Showing 3 changed files with 12 additions and 1 deletion.
diff --git a/libstainless/src/lib.rs b/libstainless/src/lib.rs
@@ -7,6 +7,10 @@ pub use set::*;
 mod map;
 pub use map::*;
 
+pub fn old<T>(t: T) -> T {
+  t
+}
+
 pub trait Implies {
   fn implies(self, b: Self) -> bool;
 }

diff --git a/stainless_extraction/src/expr/mod.rs b/stainless_extraction/src/expr/mod.rs
@@ -115,6 +115,7 @@ impl<'a, 'l, 'tcx> BodyExtractor<'a, 'l, 'tcx> {
         }
 
         StdItem::CrateItem(CrateItem::ImpliesFn) => self.extract_implies(args),
+        StdItem::CrateItem(CrateItem::OldFn) => Some(self.extract_old(args.first().unwrap())),
 
         // Box::new, erase it and return the argument directly.
         StdItem::CrateItem(BoxNewFn) => Some(self.extract_expr(args.first().unwrap())),
@@ -141,6 +142,10 @@ impl<'a, 'l, 'tcx> BodyExtractor<'a, 'l, 'tcx> {
     }
   }
 
+  fn extract_old(&mut self, arg: &'a Expr<'a, 'tcx>) -> st::Expr<'l> {
+    self.factory().Old(self.extract_expr(arg)).into()
+  }
+
   fn extract_call(
     &mut self,
     def_id: DefId,

diff --git a/stainless_extraction/src/std_items.rs b/stainless_extraction/src/std_items.rs
@@ -55,6 +55,7 @@ pub enum CrateItem {
   MapInsertFn,
   MapRemoveFn,
   OptionType,
+  OldFn,
 }
 
 use CrateItem::*;
@@ -81,6 +82,7 @@ impl CrateItem {
       CloneFn => "std::clone::Clone::clone",
       CloneTrait => "std::clone::Clone",
       ImpliesFn => "stainless::Implies::implies",
+      OldFn => "stainless::old",
       MapType => "stainless::Map",
       MapNewFn => "stainless::Map::<K, V>::new",
       MapIndexFn => "stainless::Map::<K, V>::index",
@@ -106,7 +108,7 @@ impl CrateItem {
 
   pub fn def_kind(&self) -> DefKind {
     match self {
-      BeginPanicFmtFn => DefKind::Fn,
+      BeginPanicFmtFn | OldFn => DefKind::Fn,
       SetType | MapType | StringType | PhantomData => DefKind::Struct,
       CloneTrait => DefKind::Trait,
       OptionType => DefKind::Enum,