diff --git a/src/stdlib.rs b/src/stdlib.rs index 72881c138..179b0d031 100644 --- a/src/stdlib.rs +++ b/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); diff --git a/src/types.rs b/src/types.rs index e52aa0c2d..e5c2bad3a 100644 --- a/src/types.rs +++ b/src/types.rs @@ -709,7 +709,7 @@ fn get_var_contract( impl EnumRows { fn subcontract(&self) -> Result { - 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 { @@ -775,7 +775,7 @@ impl RecordRows { pol: Polarity, sy: &mut i32, ) -> Result { - 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,8 +794,8 @@ 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!(), @@ -803,7 +803,7 @@ impl RecordRows { 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 { - 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) diff --git a/stdlib/contract.ncl b/stdlib/contract.ncl index 2671d703e..faba89401 100644 --- a/stdlib/contract.ncl +++ b/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. diff --git a/stdlib/internals.ncl b/stdlib/internals.ncl index 7a7dabf48..51796a1bc 100644 --- a/stdlib/internals.ncl +++ b/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, } diff --git a/stdlib/record.ncl b/stdlib/record.ncl index f698ca850..38c8d4507 100644 --- a/stdlib/record.ncl +++ b/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, } }