Repository: tweag/nickel
Pull request #630 (2022-03-02 16:07:56)

[Fix] Fix array/fold bench
Fix broken bench, mainly by updating the code to the latest syntax.


Patch:
diff --git a/benches/arrays.rs b/benches/arrays.rs
index d43f07ba..ca68e2d6 100644
--- a/benches/arrays.rs
+++ b/benches/arrays.rs
@@ -55,7 +55,7 @@ fn fold_arrays(c: &mut Criterion) {
         "foldr arrays 50",
         env!("CARGO_MANIFEST_DIR"),
         "arrays/fold",
-        Some("right.arrays_"),
+        Some("right.arrays"),
         50,
         EvalMode::Normal,
         c,
@@ -67,7 +67,7 @@ fn fold_arrays_deep(c: &mut Criterion) {
         "foldr deepseq arrays 30",
         env!("CARGO_MANIFEST_DIR"),
         "arrays/fold",
-        Some("right.arrays_"),
+        Some("right.arrays"),
         30,
         EvalMode::DeepSeq,
         c,
@@ -127,7 +127,7 @@ fn foldl_arrays(c: &mut Criterion) {
         "foldl arrays 50",
         env!("CARGO_MANIFEST_DIR"),
         "arrays/fold",
-        Some("left.arrays_"),
+        Some("left.arrays"),
         50,
         EvalMode::Normal,
         c,
@@ -139,7 +139,7 @@ fn foldl_arrays_deep(c: &mut Criterion) {
         "foldl deepseq arrays 30",
         env!("CARGO_MANIFEST_DIR"),
         "arrays/fold",
-        Some("left.arrays_"),
+        Some("left.arrays"),
         30,
         EvalMode::DeepSeq,
         c,
diff --git a/benches/arrays/fold.ncl b/benches/arrays/fold.ncl
index 6deab695..240bcb5c 100644
--- a/benches/arrays/fold.ncl
+++ b/benches/arrays/fold.ncl
@@ -1,4 +1,6 @@
-let letter | strings.CharLiteral -> strings.CharLiteral = fun n => strings.charFromCode (strings.charCode "a" + (n % 26)) in
+let letter | string.CharLiteral -> string.CharLiteral = fun n =>
+  string.char_code "a" + (n % 26)
+  |> string.char_from_code in
 
 {
   right = {
@@ -10,7 +12,7 @@ let letter | strings.CharLiteral -> strings.CharLiteral = fun n => strings.charF
       run = fun n =>
         array.fold (fun x y => x*y + (x - y)) (array.generate n (fun n => n/2))
     },
-    array_ = {
+    arrays = {
       run = fun n =>
         array.fold (fun x acc => [x] ++ acc) (array.generate n (fun n => [n]))
     },
@@ -24,7 +26,7 @@ let letter | strings.CharLiteral -> strings.CharLiteral = fun n => strings.charF
       run = fun n =>
         array.foldl (fun x y => x*y + (x - y)) (array.generate n (fun n => n/2))
     },
-    array_ = {
+    arrays = {
       run = fun n =>
         array.foldl (fun x acc => [x] ++ acc) (array.generate n (fun n => [n]))
     },
diff --git a/doc/manual/contracts.md b/doc/manual/contracts.md
index 5db59533..eb85ba33 100644
--- a/doc/manual/contracts.md
+++ b/doc/manual/contracts.md
@@ -433,6 +433,9 @@ error: contract broken by a value.
 [..]
 ```
 
+Recall that `Array` is an alias for `Array Dyn`, thus the `Array` contracts only
+checks that the value is an array.
+
 #### Functions
 
 A function contract `In -> Out` returns a wrapped function which, for each call,
diff --git a/doc/manual/typing.md b/doc/manual/typing.md
index 5b1b6a47..52e301d2 100644
--- a/doc/manual/typing.md
+++ b/doc/manual/typing.md
@@ -163,7 +163,8 @@ Let us now have a quick tour of the type system. The basic types are:
 
 The following type constructors are available:
 
-- **Array**: `Array T`. An array of elements of type `T`.
+- **Array**: `Array T`. An array of elements of type `T`. When no `T` is specified, `Array`
+  alone is an alias for `Array Dyn`.
 
   Example:
   ```nickel
diff --git a/src/grammar.lalrpop b/src/grammar.lalrpop
index 5f14aba2..7e0274a2 100644
--- a/src/grammar.lalrpop
+++ b/src/grammar.lalrpop
@@ -241,7 +241,6 @@ Forall: Types =
 // also includes previous levels).
 Applicative: UniTerm = {
     "import" <s: StaticString> => UniTerm::from(Term::Import(OsString::from(s))),
-    AsUniTerm<TypeArray>,
     <t1: AsTerm<Applicative>> <t2: AsTerm<RecordOperand>> =>
         UniTerm::from(mk_app!(t1, t2)),
     <op: UOp> <t: AsTerm<RecordOperand>> => UniTerm::from(mk_term::op1(op, t)),
@@ -251,9 +250,25 @@ Applicative: UniTerm = {
     RecordOperand,
 };
 
-// The parametrized array type.
-TypeArray: Types = "Array" <AsType<Atom>> =>
-    Types(AbsType::Array(Box::new(<>)));
+// The array type, potentially with an argument. Take precedence over
+// application: `Array Foo` is always interpreted as the type `Array` parametrized
+// by `Foo`, rather than the dynamic array type `Array Dyn` aliased to `Array` and
+// seen as a contract applied to term `Foo`.
+TypeArray: Types =
+    "Array" <TypeArrayParam?> => {
+        let ty = Box::new(<>.unwrap_or(Types(AbsType::Dyn())));
+        Types(AbsType::Array(ty))
+    };
+
+// Possible parameter for the array type. It's `TypeAtom` augmented with an
+// argument-less `Array`, which allows to parse `Array Array`. We can't add
+// argument-less `Array` to type atoms directly, as it would make `Array Foo`
+// ambiguous: could be parsed both as `Array` as a term applied to `Array` as a
+// term, or as the parametrized type `Array Array`).
+TypeArrayParam: Types = {
+    "Array" => Types(AbsType::Array(Box::new(Types(AbsType::Dyn())))),
+    AsType<Atom>,
+};
 
 RecordOperand: UniTerm = {
     Atom,
@@ -665,6 +680,7 @@ InfixLazyBOpApp<UOp, LExpr, RExpr>: UniTerm =
 InfixExpr: UniTerm = {
     #[precedence(level="0")]
     Applicative,
+    AsUniTerm<TypeArray>,
 
     #[precedence(level="1")]
     "-" <AsTerm<InfixExpr>> =>
diff --git a/src/typecheck/operation.rs b/src/typecheck/operation.rs
index 01cef877..127d71be 100644
--- a/src/typecheck/operation.rs
+++ b/src/typecheck/operation.rs
@@ -141,7 +141,7 @@ pub fn get_uop_type(
             //mk_tyw_record!(; TypeWrapper::Ptr(state.table.fresh_var())),
             mk_typewrapper::array(AbsType::Str()),
         ),
-        // Dyn -> Array Dyn
+        // Dyn -> Array
         UnaryOp::ValuesOf() => (
             mk_typewrapper::dynamic(),
             mk_typewrapper::array(AbsType::Dyn()),
diff --git a/src/types.rs b/src/types.rs
index 4bfe1dc0..e20af57f 100644
--- a/src/types.rs
+++ b/src/types.rs
@@ -365,7 +365,7 @@ impl Types {
 
         match &self.0 {
             Dyn() | Num() | Bool() | Str() | Var(_) => true,
-            Flat(rt) if matches!(*rt.term, Term::Var(_)) => true,
+            Array(ty) if ty.0 == AbsType::Dyn() => true,
             _ => false,
         }
     }
@@ -378,6 +378,7 @@ impl fmt::Display for Types {
             AbsType::Num() => write!(f, "Num"),
             AbsType::Bool() => write!(f, "Bool"),
             AbsType::Str() => write!(f, "Str"),
+            AbsType::Array(ty) if ty.0 == AbsType::Dyn() => write!(f, "Array"),
             AbsType::Array(ty) => {
                 write!(f, "Array ")?;
 
@@ -482,10 +483,11 @@ mod test {
         assert_format_eq("[|a, b, c, d|]");
         assert_format_eq("forall r. [|tag1, tag2, tag3 ; r|]");
 
+        assert_format_eq("Array");
         assert_format_eq("Array Num");
         assert_format_eq("Array (Array Num)");
         assert_format_eq("Num -> Array (Array Str) -> Num");
         assert_format_eq("Array (Num -> Num)");
-        assert_format_eq("Array (Array (Array Dyn) -> Num)");
+        assert_format_eq("Array (Array Array -> Num)");
     }
 }
diff --git a/stdlib/array.ncl b/stdlib/array.ncl
index 7bb1f8c2..773c16e3 100644
--- a/stdlib/array.ncl
+++ b/stdlib/array.ncl
@@ -209,7 +209,7 @@
         "%m
       = fun pred l => fold (fun x acc => if pred x then true else acc) false l,
 
-    elem : Dyn -> Array Dyn -> Bool
+    elem : Dyn -> Array -> Bool
       | doc m%"
         Results in true if the given element is a member of the array, false otherwise.
 
diff --git a/stdlib/record.ncl b/stdlib/record.ncl
index 1adf436d..64ced7fe 100644
--- a/stdlib/record.ncl
+++ b/stdlib/record.ncl
@@ -26,7 +26,7 @@
       "%m
     = fun r => %fields% r,
 
-    values | { ; Dyn} -> Array Dyn
+    values | { ; Dyn} -> Array
     | doc m%"
       Given a record, results in a array containing all the values in that record.
 


Test patch:
diff --git a/tests/contracts_fail.rs b/tests/contracts_fail.rs
index 82d6e32c..3e89390c 100644
--- a/tests/contracts_fail.rs
+++ b/tests/contracts_fail.rs
@@ -138,11 +138,11 @@ fn lists_contracts() {
         Err(Error::EvalError(EvalError::BlameError(..)))
     );
     assert_matches!(
-        eval("1 | Array Dyn"),
+        eval("1 | Array"),
         Err(Error::EvalError(EvalError::BlameError(..)))
     );
     assert_matches!(
-        eval("(fun x => x) | Array Dyn"),
+        eval("(fun x => x) | Array"),
         Err(Error::EvalError(EvalError::BlameError(..)))
     );
 
diff --git a/tests/pass/contracts.ncl b/tests/pass/contracts.ncl
index 6c408904..8fcedbe9 100644
--- a/tests/pass/contracts.ncl
+++ b/tests/pass/contracts.ncl
@@ -98,7 +98,7 @@ let Assert = fun l x => x || %blame% l in
   ({a = 0, b = 0, c = 0} | Contract) == {a = 0, b = 0, c = 0},
 
   // arrays 
-  ([1, "2", false] | Array Dyn) == [1, "2", false],
+  ([1, "2", false] | Array) == [1, "2", false],
   ([1, 2, 3] | Array Num) == [1, 2, 3],
   (["1", "2", "false"] | Array Str) == ["1", "2", "false"],
 
diff --git a/tests/pass/typechecking.ncl b/tests/pass/typechecking.ncl
index e339b523..19c9fb88 100644
--- a/tests/pass/typechecking.ncl
+++ b/tests/pass/typechecking.ncl
@@ -102,7 +102,7 @@ let typecheck = [
   // arrays_simple
   [1, "2", false],
   //TODO: the type system may accept the following test at some point.
-  //([1, "2", false] : Array Dyn),
+  //([1, "2", false] : Array),
   ["a", "b", "c"] : Array Str,
   [1, 2, 3] : Array Num,
   (fun x => [x]) : forall a. a -> Array a,
diff --git a/tests/typecheck_fail.rs b/tests/typecheck_fail.rs
index ba076801..964e6636 100644
--- a/tests/typecheck_fail.rs
+++ b/tests/typecheck_fail.rs
@@ -136,7 +136,7 @@ fn dynamic_record_simple() {
 #[test]
 fn simple_array() {
     assert_typecheck_fails!("[1, 2, false] : Array Num");
-    assert_typecheck_fails!("[(1 : Str), true, \"b\"] : Array Dyn");
+    assert_typecheck_fails!("[(1 : Str), true, \"b\"] : Array");
     assert_typecheck_fails!("[1, 2, \"3\"] : Array Str");
 }
 
@@ -144,7 +144,7 @@ fn simple_array() {
 fn arrays_operations() {
     assert_typecheck_fails!("(fun l => %head% l) : forall a b. (Array a -> b)");
     assert_typecheck_fails!(
-        "(fun f l => %elem_at% (%map% l f) 0) : forall a. (forall b. (a -> b) -> Array Dyn -> b)"
+        "(fun f l => %elem_at% (%map% l f) 0) : forall a. (forall b. (a -> b) -> Array -> b)"
     );
 }