Improve documentation.

stainless_extraction/src/expr/mod.rs

@@ -25,6 +25,7 @@ type Result<T> = std::result::Result<T, &'static str>;
 impl<'a, 'l, 'tcx> BodyExtractor<'a, 'l, 'tcx> {
   pub(super) fn extract_expr(&mut self, expr: &'a Expr<'a, 'tcx>) -> st::Expr<'l> {
     match &expr.kind {
+      // TODO: Handle arbitrary-precision integers?
       ExprKind::Literal { literal, .. } => match Literal::from_const(literal, self.tcx()) {
         Some(lit) => lit.as_st_literal(self.factory()),
         _ => self.unsupported_expr(expr.span, "Unsupported kind of literal"),
@@ -61,7 +62,6 @@ impl<'a, 'l, 'tcx> BodyExtractor<'a, 'l, 'tcx> {
       } => self.extract_if(cond, then, *else_opt),
       ExprKind::Match { scrutinee, arms } => self.extract_match(scrutinee, arms),
 
-      // TODO: Handle arbitrary-precision integers
       ExprKind::Scope { value, .. } => self.extract_expr(value),
       ExprKind::Use { source } => self.extract_expr(source),
       ExprKind::NeverToAny { source } => self.extract_expr(source),
@@ -356,6 +356,11 @@ impl<'a, 'l, 'tcx> BodyExtractor<'a, 'l, 'tcx> {
     }
   }
 
+  /// Inserts a fresh copy around the expression, if the expression can contain
+  /// mutable types. This function must only be called, when it is safe to add a
+  /// fresh copy.
+  ///
+  /// TODO: Check that fresh copy is safe for expression.
   fn extract_aliasable_expr(&mut self, expr: &'a Expr<'a, 'tcx>) -> st::Expr<'l> {
     let e = self.extract_expr(expr);
     let tpe = self.base.extract_ty(expr.ty, &self.txtcx, expr.span);

stainless_extraction/src/fns.rs

@@ -42,10 +42,6 @@ pub struct TypeClassKey<'l> {
 impl PartialEq<st::ClassType<'_>> for TypeClassKey<'_> {
   fn eq(&self, other: &st::ClassType<'_>) -> bool {
     let st::ClassType { id, tps } = other;
-    let key = TypeClassKey {
-      id: *id,
-      recv_tps: tps.clone(),
-    };
-    key == *self
+    self.id == *id && self.recv_tps == *tps
   }
 }

stainless_extraction/src/krate.rs

@@ -87,21 +87,21 @@ impl<'l, 'tcx> BaseExtractor<'l, 'tcx> {
         }
       }
 
-      /// Ignore fn items in because they are already treated when the entire
-      /// impl/trait block is extracted.
       fn visit_trait_item(&mut self, trait_item: &'tcx hir::TraitItem<'tcx>) {
         match trait_item.kind {
+          // Ignore fn items in because they are already treated when the entire
+          // impl/trait block is extracted.
           hir::TraitItemKind::Fn(..) => {}
           _ => self
             .xtor
             .unsupported(trait_item.span, "Trait item other than function"),
         }
       }
 
-      /// Ignore fn items in because they are already treated when the entire
-      /// impl/trait block is extracted.
       fn visit_impl_item(&mut self, impl_item: &'tcx hir::ImplItem<'tcx>) {
         match impl_item.kind {
+          // Ignore fn items in because they are already treated when the entire
+          // impl/trait block is extracted.
           hir::ImplItemKind::Fn(..) => {}
           _ => self
             .xtor
@@ -205,13 +205,14 @@ impl<'l, 'tcx> BaseExtractor<'l, 'tcx> {
     self.get_id_from_def(def_id).unwrap_or_else(|| {
       self.add_function_ref(def_id);
 
-      // Check whether this function implements some method of a trait.
-      // More specifically, if the function has a name
+      // Check whether this function implements some method of a trait, in other
+      // words, overrides some existing function.
       let overridden_def_id: Option<DefId> =
+        // Get the name of this function
         self.tcx.opt_item_name(def_id).and_then(|fn_item_name| {
           self
             .tcx
-            // and it is a method of an impl block
+            // Then, if it is a method of an impl block
             .impl_of_method(def_id)
             // and that impl block implements a trait
             .and_then(|impl_id| self.tcx.trait_id_of_impl(impl_id))
@@ -224,8 +225,8 @@ impl<'l, 'tcx> BaseExtractor<'l, 'tcx> {
                 trait_id,
               )
             })
-            // then we want to use that method's symbol path.
-            .map(|item| item.def_id)
+            // then we want to use the trait method's symbol path.
+            .map(|trait_item_method| trait_item_method.def_id)
         });
 
       match overridden_def_id {
@@ -255,7 +256,7 @@ impl<'l, 'tcx> BaseExtractor<'l, 'tcx> {
   }
 
   /// Extract an external function
-  pub(super) fn extract_extern_fn(&mut self, def_id: DefId) -> &'l st::FunDef<'l> {
+  fn extract_extern_fn(&mut self, def_id: DefId) -> &'l st::FunDef<'l> {
     assert!(
       !def_id.is_local(),
       "Expected non-local def id, got: {:?}",
@@ -283,7 +284,7 @@ impl<'l, 'tcx> BaseExtractor<'l, 'tcx> {
     })
   }
 
-  pub fn extract_abstract_fn(&mut self, def_id: DefId) -> &'l st::FunDef<'l> {
+  fn extract_abstract_fn(&mut self, def_id: DefId) -> &'l st::FunDef<'l> {
     let (id, tparams, params, rtp) = self.extract_fn_signature(def_id);
     let class_def = self.get_class_of_method(id);
 
@@ -344,7 +345,7 @@ impl<'l, 'tcx> BaseExtractor<'l, 'tcx> {
   }
 
   /// Extract a local function
-  pub(super) fn extract_local_fn(&mut self, fn_item: &FnItem<'l>) -> &'l st::FunDef<'l> {
+  fn extract_local_fn(&mut self, fn_item: &FnItem<'l>) -> &'l st::FunDef<'l> {
     let f = self.factory();
     let tcx = self.tcx;
 
@@ -519,7 +520,9 @@ impl<'l, 'tcx> BaseExtractor<'l, 'tcx> {
               .remove(&field.ident.name)
               .map(|flags| flags.to_stainless(f))
               .unwrap_or_default();
+            // All fields are potentially mutable in Rust
             flags.push(f.IsVar().into());
+
             let field = f.Variable(field_id, field_ty, flags);
             &*f.ValDef(field)
           })

stainless_extraction/src/lib.rs

@@ -265,9 +265,9 @@ impl<'l, 'tcx> BaseExtractor<'l, 'tcx> {
     })
   }
 
-  /// Return a reference to the class definition on which the given function is
-  /// defined as method. If the function is not a method, None is returned. The
-  /// function is identified by its id.
+  /// Return a reference to the class definition on which the given function
+  /// (identified by its id) is defined as method. If the function is not a
+  /// method, None is returned.
   fn get_class_of_method(&mut self, id: StainlessSymId<'l>) -> Option<&'l st::ClassDef<'l>> {
     self.with_extraction(|xt| xt.method_to_class.get(&id).copied())
   }
@@ -336,11 +336,10 @@ impl<'l, 'tcx> BaseExtractor<'l, 'tcx> {
   /// Error reporting helpers
 
   fn unsupported<S: Into<MultiSpan>, M: Into<String>>(&self, span: S, msg: M) {
-    let msg = msg.into();
     self
       .tcx
       .sess
-      .span_err(span, format!("Unsupported tree: {}", msg).as_str());
+      .span_err(span, format!("Unsupported tree: {}", msg.into()).as_str());
   }
 }
 

stainless_extraction/src/ty.rs

@@ -214,7 +214,8 @@ impl<'l, 'tcx> BaseExtractor<'l, 'tcx> {
 
     // Discovering HOF parameters.
     // We extract `F: Fn*(S) -> T` trait predicates by replacing `F` by `S => T`.
-    // We also enumerate all other predicates, complain about all but the obviously innocuous ones.
+    // We also enumerate all other predicates and use them as trait bounds or
+    // complain about all but the obviously innocuous ones.
     let mut tparam_to_fun_params: HashMap<u32, (Vec<Ty<'tcx>>, Span)> = HashMap::new();
     let mut tparam_to_fun_return: HashMap<u32, (Ty<'tcx>, Span)> = HashMap::new();
     let mut trait_bounds: HashSet<(TraitRef<'tcx>, Span)> = HashSet::new();