From 4455a63f403b139ed8e6ad18fc949b4f13f3d43e Mon Sep 17 00:00:00 2001 From: Yann Hamdaoui Date: Mon, 27 Mar 2023 13:09:45 +0200 Subject: [PATCH 1/3] WIP --- src/stdlib.rs | 15 +++++++++----- src/types.rs | 38 +++++++++++++++++------------------ stdlib/contract.ncl | 48 +++++++++++++++++++++++++++++++++++++++++++++ stdlib/record.ncl | 14 +++++++++++++ 4 files changed, 91 insertions(+), 24 deletions(-) diff --git a/src/stdlib.rs b/src/stdlib.rs index 72881c138..099a6bf4c 100644 --- a/src/stdlib.rs +++ b/src/stdlib.rs @@ -110,8 +110,9 @@ macro_rules! generate_accessor { }; } -/// Accessors to the builtin contracts. -pub mod contract { +/// Accessors to the builtin contracts and other internals operations that aren't accessible from +/// user code. +pub mod internals { use super::*; // `dyn` is a reserved keyword in rust @@ -135,11 +136,15 @@ pub mod contract { generate_accessor!(forall_tail); generate_accessor!(dyn_tail); generate_accessor!(empty_tail); + + generate_accessor!(rec_default); + generate_accessor!(rec_force); } -pub mod internals { +pub mod contract { use super::*; - generate_accessor!(rec_default); - generate_accessor!(rec_force); + pub fn equal() -> RichTerm { + mk_term::op1(UnaryOp::StaticAccess(Ident::from("contract")), mk_term::var("x")), + } } 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..b19e92a7a 100644 --- a/stdlib/contract.ncl +++ b/stdlib/contract.ncl @@ -1,5 +1,53 @@ { 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 test + that the size is the same for arrays and that fields are the same for + records), but return 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 `%{%length% constant}`, got `%{value_length}`)" + |> label.append_note "`Equal constant` requires that the checked value is equal to the array `constant`, but their lengths differ.`" + |> blame + else + blame_with_message + "expected array, got %{builtin.typeof value}" + label, + # Outside of datastructures, we just use (==) + _ => from_predicate ((==) constant), + }, + blame | doc m%" Raise blame for a given label. diff --git a/stdlib/record.ncl b/stdlib/record.ncl index f698ca850..519ac77a0 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 cound 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, } } From e53a4224e19912706ee077c9683d3daac89e8fa7 Mon Sep 17 00:00:00 2001 From: Yann Hamdaoui Date: Mon, 27 Mar 2023 16:05:06 +0200 Subject: [PATCH 2/3] Add Equal contract Add an Equal contract to the stdlib, which checks that the value is equal to some constant. This contracts try to preserve laziness, in that checks are delayed for arrays and records in principle. Caution: currently, the lazy check isn't implemented for record, so this contract is actually just `fun c => from_predicate ((==) c)` when `c` is a record, temporarily. --- src/stdlib.rs | 12 ++---------- stdlib/contract.ncl | 13 +++++++------ stdlib/internals.ncl | 7 +++++++ 3 files changed, 16 insertions(+), 16 deletions(-) diff --git a/src/stdlib.rs b/src/stdlib.rs index 099a6bf4c..179b0d031 100644 --- a/src/stdlib.rs +++ b/src/stdlib.rs @@ -110,8 +110,7 @@ macro_rules! generate_accessor { }; } -/// Accessors to the builtin contracts and other internals operations that aren't accessible from -/// user code. +/// Accessors to the builtin contracts and other internals that aren't accessible from user code. pub mod internals { use super::*; @@ -136,15 +135,8 @@ pub mod internals { generate_accessor!(forall_tail); generate_accessor!(dyn_tail); generate_accessor!(empty_tail); + generate_accessor!(contract_equal); generate_accessor!(rec_default); generate_accessor!(rec_force); } - -pub mod contract { - use super::*; - - pub fn equal() -> RichTerm { - mk_term::op1(UnaryOp::StaticAccess(Ident::from("contract")), mk_term::var("x")), - } -} diff --git a/stdlib/contract.ncl b/stdlib/contract.ncl index b19e92a7a..410f3bba8 100644 --- a/stdlib/contract.ncl +++ b/stdlib/contract.ncl @@ -37,14 +37,15 @@ contract.apply (Equal (%elem_at% constant i)) label' value) else label' - |> label.with_message "array length mismatch (expected `%{%length% constant}`, got `%{value_length}`)" - |> label.append_note "`Equal constant` requires that the checked value is equal to the array `constant`, but their lengths differ.`" + |> 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 - blame_with_message - "expected array, got %{builtin.typeof value}" - label, - # Outside of datastructures, we just use (==) + 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), }, diff --git a/stdlib/internals.ncl b/stdlib/internals.ncl index 7a7dabf48..b7a457bda 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 an 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 prevent it from being shadowed. + "$stdlib_contract_equal" = contract.Equal, } From 4e7f11b6ffb5801c5f636cf22ea629b4a4af7c31 Mon Sep 17 00:00:00 2001 From: Yann Hamdaoui Date: Tue, 28 Mar 2023 10:42:12 +0200 Subject: [PATCH 3/3] Apply suggestions from code review Fix typos in the code documentation Co-authored-by: Viktor Kleen --- stdlib/contract.ncl | 4 ++-- stdlib/internals.ncl | 4 ++-- stdlib/record.ncl | 2 +- 3 files changed, 5 insertions(+), 5 deletions(-) diff --git a/stdlib/contract.ncl b/stdlib/contract.ncl index 410f3bba8..faba89401 100644 --- a/stdlib/contract.ncl +++ b/stdlib/contract.ncl @@ -5,9 +5,9 @@ `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 test + `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 return a new value where an equality contract has been + records), but returns a new value where an equality contract has been pushed down each element. # Example diff --git a/stdlib/internals.ncl b/stdlib/internals.ncl index b7a457bda..51796a1bc 100644 --- a/stdlib/internals.ncl +++ b/stdlib/internals.ncl @@ -147,10 +147,10 @@ "$rec_force" = fun value => %rec_force% (%force% value), "$rec_default" = fun value => %rec_default% (%force% value), - # Provide an access to contract.Equal within the initial environement. Merging + # 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 prevent it from being shadowed. + # environment and prevents it from being shadowed. "$stdlib_contract_equal" = contract.Equal, } diff --git a/stdlib/record.ncl b/stdlib/record.ncl index 519ac77a0..38c8d4507 100644 --- a/stdlib/record.ncl +++ b/stdlib/record.ncl @@ -199,7 +199,7 @@ length : forall a. {_: a} -> Number | doc m%" - Returns the number of fields in a record. This cound doesn't include + 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