Add Equal contract to the stdlib

src/stdlib.rs

@@ -110,8 +110,8 @@ macro_rules! generate_accessor {
     };
 }
 
-/// Accessors to the builtin contracts.
-pub mod contract {
+/// Accessors to the builtin contracts and other internals that aren't accessible from user code.
+pub mod internals {
     use super::*;
 
     // `dyn` is a reserved keyword in rust
@@ -135,10 +135,7 @@ pub mod contract {
     generate_accessor!(forall_tail);
     generate_accessor!(dyn_tail);
     generate_accessor!(empty_tail);
-}
-
-pub mod internals {
-    use super::*;
+    generate_accessor!(contract_equal);
 
     generate_accessor!(rec_default);
     generate_accessor!(rec_force);

src/types.rs

@@ -709,7 +709,7 @@ fn get_var_contract(
 
 impl EnumRows {
     fn subcontract(&self) -> Result<RichTerm, UnboundTypeVariableError> {
-        use crate::stdlib::contract;
+        use crate::stdlib::internals;
 
         let mut cases = HashMap::new();
         let mut has_tail = false;
@@ -752,14 +752,14 @@ impl EnumRows {
             mk_app!(
                 Term::Match {
                     cases,
-                    default: Some(mk_app!(contract::enum_fail(), mk_term::var(label_arg))),
+                    default: Some(mk_app!(internals::enum_fail(), mk_term::var(label_arg))),
                 },
                 mk_term::var(value_arg)
             )
         };
         let case = mk_fun!(label_arg, value_arg, case_body);
 
-        Ok(mk_app!(contract::enums(), case))
+        Ok(mk_app!(internals::enums(), case))
     }
 
     pub fn iter(&self) -> EnumRowsIterator<EnumRows> {
@@ -775,7 +775,7 @@ impl RecordRows {
         pol: Polarity,
         sy: &mut i32,
     ) -> Result<RichTerm, UnboundTypeVariableError> {
-        use crate::stdlib::contract;
+        use crate::stdlib::internals;
 
         // We begin by building a record whose arguments are contracts
         // derived from the types of the statically known fields.
@@ -794,16 +794,16 @@ impl RecordRows {
         // Now that we've dealt with the row extends, we just need to
         // work out the tail.
         let tail = match &rrows.0 {
-            RecordRowsF::Empty => contract::empty_tail(),
-            RecordRowsF::TailDyn => contract::dyn_tail(),
+            RecordRowsF::Empty => internals::empty_tail(),
+            RecordRowsF::TailDyn => internals::dyn_tail(),
             RecordRowsF::TailVar(id) => get_var_contract(&vars, id)?,
             // Safety: the while above excludes that `tail` can have the form `Extend`.
             RecordRowsF::Extend { .. } => unreachable!(),
         };
 
         let rec = RichTerm::from(Term::Record(RecordData::with_field_values(fcs)));
 
-        Ok(mk_app!(contract::record(), rec, tail))
+        Ok(mk_app!(internals::record(), rec, tail))
     }
 
     /// Find a nested binding in a record row type. The nested field is given as a list of
@@ -903,19 +903,19 @@ impl Types {
         pol: Polarity,
         sy: &mut i32,
     ) -> Result<RichTerm, UnboundTypeVariableError> {
-        use crate::stdlib::contract;
+        use crate::stdlib::internals;
 
         let ctr = match self.types {
-            TypeF::Dyn => contract::dynamic(),
-            TypeF::Number => contract::num(),
-            TypeF::Bool => contract::bool(),
-            TypeF::String => contract::string(),
+            TypeF::Dyn => internals::dynamic(),
+            TypeF::Number => internals::num(),
+            TypeF::Bool => internals::bool(),
+            TypeF::String => internals::string(),
             //TODO: optimization: have a specialized contract for `Array Dyn`, to avoid mapping an
             //always successful contract on each element.
-            TypeF::Array(ref ty) => mk_app!(contract::array(), ty.subcontract(vars, pol, sy)?),
+            TypeF::Array(ref ty) => mk_app!(internals::array(), ty.subcontract(vars, pol, sy)?),
             TypeF::Symbol => panic!("Are you trying to check a Sym at runtime?"),
             TypeF::Arrow(ref s, ref t) => mk_app!(
-                contract::func(),
+                internals::func(),
                 s.subcontract(vars.clone(), pol.flip(), sy)?,
                 t.subcontract(vars, pol, sy)?
             ),
@@ -930,14 +930,14 @@ impl Types {
 
                 let sealing_key = Term::SealingKey(*sy);
                 let contract = match var_kind {
-                    Type => mk_app!(contract::forall_var(), sealing_key.clone()),
-                    EnumRows | RecordRows => mk_app!(contract::forall_tail(), sealing_key.clone()),
+                    Type => mk_app!(internals::forall_var(), sealing_key.clone()),
+                    EnumRows | RecordRows => mk_app!(internals::forall_tail(), sealing_key.clone()),
                 };
                 vars.insert(*var, contract);
 
                 *sy += 1;
                 mk_app!(
-                    contract::forall(),
+                    internals::forall(),
                     sealing_key,
                     Term::from(pol),
                     body.subcontract(vars, pol, sy)?
@@ -946,9 +946,9 @@ impl Types {
             TypeF::Enum(ref erows) => erows.subcontract()?,
             TypeF::Record(ref rrows) => rrows.subcontract(vars, pol, sy)?,
             TypeF::Dict(ref ty) => {
-                mk_app!(contract::dyn_record(), ty.subcontract(vars, pol, sy)?)
+                mk_app!(internals::dyn_record(), ty.subcontract(vars, pol, sy)?)
             }
-            TypeF::Wildcard(_) => contract::dynamic(),
+            TypeF::Wildcard(_) => internals::dynamic(),
         };
 
         Ok(ctr)

stdlib/contract.ncl

@@ -1,5 +1,54 @@
 {
   contract = {
+    Equal
+      | doc m%"
+        `Equal` is a contract enforcing equality to a given constant.
+
+        `Equal` is lazy over arrays and records. When checking such values,
+        `Equal` doesn't test for equality of elements right away (it just tests
+        that the size is the same for arrays and that fields are the same for
+        records), but returns a new value where an equality contract has been
+        pushed down each element.
+
+        # Example
+
+        ```nickel
+        1 + 4 | Equal 5
+         => 5
+        4 | Equal 5
+         => ERROR (contract broken by a value)
+        ```
+      "%
+    = fun constant =>
+      %typeof% constant
+      |> match {
+        `Record =>
+          #TODO: lazy version for records. The difficulty is not to make it lazy
+          #right now, but to make it preserve recursivity as well. We might need
+          #something like a recursivity-preserving map, or a primop for
+          # per-field contract application, like %array_lazy_assume%.
+          from_predicate ((==) constant),
+        `Array =>
+          fun label' value =>
+            if %typeof% value == `Array then
+              let value_length = %length% value in
+              if value_length == %length% constant then
+                %generate% value_length (fun i =>
+                  contract.apply (Equal (%elem_at% constant i)) label' value)
+              else
+                label'
+                |> label.with_message "array length mismatch (expected `%{%to_str% (%length% constant)}`, got `%{%to_str% value_length}`)"
+                |> label.append_note "`Equal some_array` requires that the checked value is equal to the array `some_array`, but their lengths differ."
+                |> blame
+            else
+              label'
+                |> label.with_message "expected Array, got %{%to_str% (%typeof% value)}"
+                |> label.append_note "`Equal some_array` requires that the checked value is equal to the array `some_array`, but the provided value isn't an array."
+                |> blame,
+        # Outside of lazy data structure, we just use (==)
+        _ => from_predicate ((==) constant),
+      },
+
     blame
       | doc m%"
         Raise blame for a given label.

stdlib/internals.ncl

@@ -146,4 +146,11 @@
 
   "$rec_force" = fun value => %rec_force% (%force% value),
   "$rec_default" = fun value => %rec_default% (%force% value),
+
+  # Provide access to contract.Equal within the initial environement. Merging
+  # makes use of `contract.Equal`, but it can't blindly substitute such an
+  # expression, because `contract` might have been redefined locally. Putting it
+  # in an internal value prefixed with `$` makes it accessible from the initial
+  # environment and prevents it from being shadowed.
+  "$stdlib_contract_equal" = contract.Equal,
 }

stdlib/record.ncl

@@ -195,5 +195,19 @@
       |> to_array
       |> array.filter (fun { field, value } => f field value)
       |> from_array,
+
+    length
+      : forall a. {_: a} -> Number
+      | doc m%"
+          Returns the number of fields in a record. This count doesn't include
+          fields both marked as optional and without a definition.
+
+          Because of the need to filter empty optional fields, the cost of
+          `length` is linear in the size of the record.
+        "%
+      = fun record =>
+        record
+        |> fields
+        |> array.length,
   }
 }