Add tests of contract for dynamic row tail
@@ -1410,9 +1410,6 @@ Assume(#alwaysTrue -> #alwaysFalse, not ) true
.unwrap_err();
}
- #[test]
- fn records_contracts_dyn() {}
-
#[test]
fn records_contracts_poly() {
let id = "let f = Assume(forall a. { | a} -> { | a }, fun x => x) in f";
@@ -1472,6 +1469,23 @@ Assume(#alwaysTrue -> #alwaysFalse, not ) true
.unwrap_err();
}
+ #[test]
+ fn records_contracts_dyn() {
+ assert_peq!(
+ "Assume({a: Num, b: Str | Dyn}, {a = 1; b = \"b\"})",
+ "{a = 1; b = \"b\"}"
+ );
+ assert_peq!(
+ "Assume({a: Num, b: Str | Dyn}, {a = 1; b = \"b\"; c = false})",
+ "{a = 1; b = \"b\"; c = false}"
+ );
+ assert_peq!(
+ "Assume({a: Num | Dyn} -> Dyn, fun r => r.b) {a = 1; b = 2}",
+ "{a = 1; b = 2}"
+ );
+ eval_string("Assume({a: Num, b: Str | Dyn}, {a = 1})").unwrap_err();
+ }
+
#[test]
fn multiline_string_indent() {
// /!\ Trailing spaces on the first line are on purpose, don't remove ! /!\
