Rebase stainless and inox dependency

.stainless-version

@@ -1 +1 @@
-noxt-0.7.1-21-g381fb00
+noxt-0.7.6-67-g533f5d5

demo/examples/adts.rs

@@ -1,3 +1,5 @@
+extern crate stainless;
+
 // In rustc's HIR all of the following make_* functions contain somewhat
 // distinct trees. Here's a succinct overview of the cases I think we'd like to
 // consider in the short term:
@@ -14,13 +16,13 @@ pub struct Foo2(i32, bool);
 
 pub struct Foo3 {
   a: i32,
-  b: bool
+  b: bool,
 }
 
 pub enum Bar {
   Bar1,
   Bar2(i32, bool),
-  Bar3 { c: i32, d: bool }
+  Bar3 { c: i32, d: bool },
 }
 
 fn make_foo1() -> Foo1 {
@@ -51,35 +53,35 @@ fn get_i32_from_bar(bar: Bar) -> i32 {
   match bar {
     Bar::Bar1 => 0,
     Bar::Bar2(c, _) => c,
-    Bar::Bar3 { c, .. } => c
+    Bar::Bar3 { c, .. } => c,
   }
 }
 
 fn get_bool_from_bar(bar: Bar) -> bool {
   match bar {
     Bar::Bar1 => false,
     Bar::Bar2(_, d) => d,
-    Bar::Bar3 { d, .. } => d
+    Bar::Bar3 { d, .. } => d,
   }
 }
 
-fn main() -> () {
+pub fn main() -> () {
   match make_foo1() {
-    Foo1 => ()
+    Foo1 => (),
   };
 
   let foo2 = make_foo2();
   foo2.0;
   foo2.1;
   match foo2 {
-    Foo2(a, b) => (a, b)
+    Foo2(a, b) => (a, b),
   };
 
   let foo3 = make_foo3();
   foo3.a;
   foo3.b;
   match foo3 {
-    Foo3 { a, b } => (a, b)
+    Foo3 { a, b } => (a, b),
   };
 
   get_i32_from_bar(make_bar1());

demo/examples/type_class.rs

@@ -10,7 +10,6 @@ trait Equals {
   // - trait => abstract class
   // - take trait with all type params, add one new at the end
   // => abstract class Equals[T]
-
   fn equals(&self, x: &Self) -> bool;
 
   // type_class_insts: Map( ("Equals", "Self", []) -> "this" )
@@ -36,24 +35,48 @@ trait Equals {
   }
 }
 
+/*
+- 'impl<..> Z for X' and has type params => case class
+- impl<tps> => ListEquals[tps]
+- trait bounds => trait bounds implemented by evidence params
+- the trait with as last type param the 'for X' => extends trait[..., X]
+(the last two use the same translation)
+=> case class ListEquals[T](ev: Equals[T]) extends Equals[List[T]]
+*/
+
 impl<T: Equals> Equals for List<T> {
-  /*
-  - 'impl<..> Z for X' and has type params => case class
-  - impl<tps> => ListEquals[tps]
-  - trait bounds => trait bounds implemented by evidence params
-  - the trait with as last type param the 'for X' => extends trait[..., X]
-  (the last two use the same translation)
-  => case class ListEquals[T](ev: Equals[T]) extends Equals[List[T]]
-  */
-
-  // #[measure(self)]
   fn equals(&self, other: &List<T>) -> bool {
     match (self, other) {
       (List::Nil, List::Nil) => true,
       (List::Cons(x, xs), List::Cons(y, ys)) => x.equals(y) && xs.equals(ys),
       _ => false,
     }
   }
+
+  fn law_reflexive(x: &Self) -> bool {
+    match x {
+      List::Cons(x, xs) => T::law_reflexive(x) && Self::law_reflexive(xs),
+      List::Nil => true,
+    }
+  }
+
+  fn law_symmetric(x: &Self, y: &Self) -> bool {
+    match (x, y) {
+      (List::Cons(x, xs), List::Cons(y, ys)) => {
+        T::law_symmetric(x, y) && Self::law_symmetric(xs, ys)
+      }
+      _ => true,
+    }
+  }
+
+  fn law_transitive(x: &Self, y: &Self, z: &Self) -> bool {
+    match (x, y, z) {
+      (List::Cons(x, xs), List::Cons(y, ys), List::Cons(z, zs)) => {
+        T::law_transitive(x, y, z) && Self::law_transitive(xs, ys, zs)
+      }
+      _ => true,
+    }
+  }
 }
 
 // case object IntEquals extends Equals[i32]
@@ -65,31 +88,12 @@ impl Equals for i32 {
   }
 }
 
-trait Ord: Equals {
-  fn less_than_eq(&self, other: &Self) -> bool;
-
-  fn less_than(&self, other: &Self) -> bool {
-    self.less_than_eq(other) && self.not_equals(other)
-  }
-}
-
-impl Ord for i32 {
-  fn less_than_eq(&self, other: &Self) -> bool {
-    self <= other
-  }
-
-  fn less_than(&self, other: &Self) -> bool {
-    self < other
-  }
-}
-
 pub fn main() {
   let a = 2;
   let b = 4;
 
   // => IntEquals.equals(a, b)
   assert!(a.not_equals(&b));
-  assert!(a.less_than(&b));
 
   // => ListEquals.equals(list, list)(IntEquals)
   let list = List::Cons(123, Box::new(List::Cons(456, Box::new(List::Nil))));
@@ -118,48 +122,17 @@ abstract class Equals[T] {
 
 case class ListEquals[A](ev: Equals[A]) extends Equals[List[A]] {
   def equals(xs: List[A], ys: List[A]): Boolean = {
-    decreases(xs.size)
     (xs, ys) match {
       case (Cons(x, xs), Cons(y, ys)) => ev.equals(x, y) && equals(xs, ys)
       case (Nil(), Nil()) => true
       case _ => false
     }
   }
+
+  // will also require manual proofs of the laws
 }
 
 case object IntEquals extends Equals[Int] {
   def equals(x: Int, y: Int): Boolean = x == y
 }
-
-// stainless extracts this as follows
-
- Symbols before PartialFunctions
-
--------------Functions-------------
-@abstract
-@method(Equals)
-def equals(x: T, y: T): Boolean = <empty tree>[Boolean]
-
-@law
-@method(Equals)
-def law_transitive(x: T, y: T, z: T): Boolean = ¬(this.equals(x, y) && this.equals(y, z)) || this.equals(x, z)
-
-@law
-@method(Equals)
-def law_symmetric(x: T, y: T): Boolean = this.equals(x, y) == this.equals(y, x)
-
-@method(IntEquals)
-def equals(x: Int, y: Int): Boolean = x == y
-
-@law
-@method(Equals)
-def law_reflexive(x: T): Boolean = this.equals(x, x)
-
--------------Classes-------------
-@caseObject
-case class IntEquals extends Equals[Int]
-
-@abstract
-abstract class Equals[T]
-
 */

stainless_backend/src/lib.rs

@@ -56,20 +56,18 @@ impl Backend {
       .arg("--interactive")
       .arg("--batched")
       .arg("--vc-cache=false")
+      .arg("--type-checker=false")
       .arg(format!("--timeout={}", config.timeout))
       .arg(format!("--print-ids={}", config.print_ids))
       .arg(format!("--print-types={}", config.print_types))
-      .arg(format!("--strict-arithmetic={}", config.strict_arithmetic))
-      // FIXME: Turn the measure inference back on as soon as
-      //   https://github.com/epfl-lara/rust-stainless/issues/68
-      //   is solved.
-      .arg("--infer-measures=no")
-      .arg("--check-measures=false");
+      .arg(format!("--strict-arithmetic={}", config.strict_arithmetic));
+
     if config.debug_trees {
       cmd
         .arg("--debug=trees")
         .arg(format!("--debug-phases={}", config.debug_phases.join(",")));
     }
+
     if let Ok(extra_flags) = env::var("STAINLESS_FLAGS") {
       cmd.args(extra_flags.split(' '));
     }

stainless_frontend/tests/pass/type_class.rs

@@ -45,7 +45,6 @@ trait Equals {
 */
 
 impl<T: Equals> Equals for List<T> {
-  // #[measure(self)]
   fn equals(&self, other: &List<T>) -> bool {
     match (self, other) {
       (List::Nil, List::Nil) => true,
@@ -97,8 +96,8 @@ pub fn main() {
   assert!(a.not_equals(&b));
 
   // => ListEquals.equals(list, list)(IntEquals)
-  // let list = List::Cons(123, Box::new(List::Cons(456, Box::new(List::Nil))));
-  // assert!(list.equals(&list));
+  let list = List::Cons(123, Box::new(List::Cons(456, Box::new(List::Nil))));
+  assert!(list.equals(&list));
 }
 
 /*
@@ -123,13 +122,14 @@ abstract class Equals[T] {
 
 case class ListEquals[A](ev: Equals[A]) extends Equals[List[A]] {
   def equals(xs: List[A], ys: List[A]): Boolean = {
-    decreases(xs.size)
     (xs, ys) match {
       case (Cons(x, xs), Cons(y, ys)) => ev.equals(x, y) && equals(xs, ys)
       case (Nil(), Nil()) => true
       case _ => false
     }
   }
+
+  // will also require manual proofs of the laws
 }
 
 case object IntEquals extends Equals[Int] {