tweag/nickel
1
1
Fork 0
mirror of https://github.com/tweag/nickel.git synced 2024-11-10 10:46:49 +03:00
Code Issues Projects Releases Wiki Activity

Merge pull request #247 from tweag/task/eq-operator

Browse Source 
Built-in evaluation of a sequence of equalities
This commit is contained in:
Yann Hamdaoui 2020-12-18 10:55:05 +00:00 committed by GitHub
commit 732d30189e
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
4 changed files with 219 additions and 77 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

197
src/operation.rs
View File

@ -15,16 +15,31 @@ use crate::merge;
use crate::merge::merge;
use crate::position::RawSpan;
use crate::stack::Stack;
use crate::stdlib;
use crate::term::make as mk_term;
use crate::term::{BinaryOp, RichTerm, StrChunk, Term, UnaryOp};
use crate::transformations::Closurizable;
use crate::{mk_app, mk_fun};
use simple_counter::*;
use std::collections::HashMap;
use std::iter::Extend;
generate_counter!(FreshVariableCounter, usize);
/// Result of the equality of two terms.
///
/// The equality of two terms can either be computed directly for base types (`Num`, `Str`, etc.),
/// in which case `Bool` is returned. Otherwise, composite values such as lists or records generate
/// new subequalities, as represented by the last variant as a vector of pairs of terms. This list
/// should be non-empty (it if was empty, `eq` should have returned `Bool(true)` directly). The
/// first element of this non-empty list is encoded as the two first parameters of `Eqs`, while the
/// last vector parameter is the (potentially empty) tail.
///
/// See [`eq`](./fn.eq.html).
enum EqResult {
Bool(bool),
Eqs(RichTerm, RichTerm, Vec<(Closure, Closure)>),
}
/// An operation continuation as stored on the stack.
#[derive(Debug, PartialEq)]
pub enum OperationCont {
@ -623,7 +638,7 @@ fn process_binary_operation(
fst_pos: Option<RawSpan>,
clos: Closure,
snd_pos: Option<RawSpan>,
_stack: &mut Stack,
stack: &mut Stack,
pos_op: Option<RawSpan>,
) -> Result<Closure, EvalError> {
let Closure {
@ -838,64 +853,49 @@ fn process_binary_operation(
}
}
BinaryOp::Eq() => {
/// Take an iterator of pairs of RichTerm, the common environments of all left
/// components of these pairs and all right components, the final environment,
/// and build a Term which evaluates to `Bool(true)` if and only if all the pairs are
/// equals
fn eq_all<T>(
it: T,
env1: &Environment,
env2: &Environment,
env: &mut Environment,
) -> Term
where
T: Iterator<Item = (RichTerm, RichTerm)>,
{
let subeqs: Vec<RichTerm> = it
.map(|(t1, t2)| {
let t1_var = t1.closurize(env, env1.clone());
let t2_var = t2.closurize(env, env2.clone());
Term::Op2(BinaryOp::Eq(), t1_var, t2_var).into()
})
.collect();
// lists.all (fun x => x) subeqs
Term::App(
mk_app!(stdlib::lists::all(), mk_term::id()),
Term::List(subeqs).into(),
)
}
let mut env = Environment::new();
let mut env: Environment = HashMap::new();
let res = match (*t1, *t2) {
(Term::Bool(b1), Term::Bool(b2)) => Term::Bool(b1 == b2),
(Term::Num(n1), Term::Num(n2)) => Term::Bool(n1 == n2),
(Term::Str(s1), Term::Str(s2)) => Term::Bool(s1 == s2),
(Term::Lbl(l1), Term::Lbl(l2)) => Term::Bool(l1 == l2),
(Term::Sym(s1), Term::Sym(s2)) => Term::Bool(s1 == s2),
(Term::Record(m1), Term::Record(m2)) => {
let (left, center, right) = merge::hashmap::split(m1, m2);
if !left.is_empty() || !right.is_empty() {
Term::Bool(false)
} else {
eq_all(
center.into_iter().map(|(_, (t1, t2))| (t1, t2)),
&env1,
&env2,
&mut env,
)
}
}
(Term::List(l1), Term::List(l2)) if l1.len() == l2.len() => {
eq_all(l1.into_iter().zip(l2.into_iter()), &env1, &env2, &mut env)
}
(_, _) => Term::Bool(false),
let c1 = Closure {
body: RichTerm {
term: t1,
pos: pos1,
},
env: env1,
};
let c2 = Closure {
body: RichTerm {
term: t2,
pos: pos2,
},
env: env2,
};
Ok(Closure {
body: res.into(),
env,
})
match eq(&mut env, c1, c2) {
EqResult::Bool(b) => match (b, stack.pop_eq()) {
(false, _) => {
stack.clear_eqs();
Ok(Closure::atomic_closure(Term::Bool(false).into()))
}
(true, None) => Ok(Closure::atomic_closure(Term::Bool(true).into())),
(true, Some((c1, c2))) => {
let t1 = c1.body.closurize(&mut env, c1.env);
let t2 = c2.body.closurize(&mut env, c2.env);
Ok(Closure {
body: RichTerm::new(Term::Op2(BinaryOp::Eq(), t1, t2), pos_op),
env,
})
}
},
EqResult::Eqs(t1, t2, subeqs) => {
stack.push_eqs(subeqs.into_iter());
Ok(Closure {
body: RichTerm::new(Term::Op2(BinaryOp::Eq(), t1, t2), pos_op),
env,
})
}
}
}
BinaryOp::LessThan() => {
if let Term::Num(n1) = *t1 {
@ -1257,6 +1257,89 @@ fn process_binary_operation(
}
}
/// Compute the equality of two terms, represented as closures.
///
/// # Parameters
///
/// - env: the final environment in which to closurize the operands of potential subequalities.
/// - c1: the closure of the first operand.
/// - c2: the closure of the second operand.
///
/// # Return
///
/// Return either a boolean when the equality can be computed directly, or a new non-empty list of equalities to be checked if
/// operands are composite values.
fn eq(env: &mut Environment, c1: Closure, c2: Closure) -> EqResult {
let Closure {
body: RichTerm { term: t1, .. },
env: env1,
} = c1;
let Closure {
body: RichTerm { term: t2, .. },
env: env2,
} = c2;
// Take a list of subequalities, and either return `EqResult::Bool(true)` if it is empty, or
// generate an approriate `EqResult::Eqs` variant with closurized terms in it.
fn gen_eqs<I>(
mut it: I,
env: &mut Environment,
env1: Environment,
env2: Environment,
) -> EqResult
where
I: Iterator<Item = (RichTerm, RichTerm)>,
{
if let Some((t1, t2)) = it.next() {
let eqs = it
.map(|(t1, t2)| {
(
Closure {
body: t1,
env: env1.clone(),
},
Closure {
body: t2,
env: env2.clone(),
},
)
})
.collect();
EqResult::Eqs(t1.closurize(env, env1), t2.closurize(env, env2), eqs)
} else {
EqResult::Bool(true)
}
}
match (*t1, *t2) {
(Term::Bool(b1), Term::Bool(b2)) => EqResult::Bool(b1 == b2),
(Term::Num(n1), Term::Num(n2)) => EqResult::Bool(n1 == n2),
(Term::Str(s1), Term::Str(s2)) => EqResult::Bool(s1 == s2),
(Term::Lbl(l1), Term::Lbl(l2)) => EqResult::Bool(l1 == l2),
(Term::Sym(s1), Term::Sym(s2)) => EqResult::Bool(s1 == s2),
(Term::Record(m1), Term::Record(m2)) => {
let (left, center, right) = merge::hashmap::split(m1, m2);
if !left.is_empty() || !right.is_empty() {
EqResult::Bool(false)
} else if center.is_empty() {
EqResult::Bool(true)
} else {
let eqs = center.into_iter().map(|(_, (t1, t2))| (t1, t2));
gen_eqs(eqs.into_iter(), env, env1, env2)
}
}
(Term::List(l1), Term::List(l2)) if l1.len() == l2.len() => {
// Equalities are tested in reverse order, but that shouldn't matter. If it
// does, just do `eqs.rev()`
let eqs = l1.into_iter().zip(l2.into_iter());
gen_eqs(eqs.into_iter(), env, env1, env2)
}
(_, _) => EqResult::Bool(false),
}
}
#[cfg(test)]
mod tests {
use super::*;

27
src/program.rs
View File

@ -1307,6 +1307,33 @@ Assume(#alwaysTrue, false)
assert_npeq!("{ a = { a = true } }", "{a = { a = { a = true } } }");
}
// Now that the equality operator directly uses the stack to store its continuation (see
// https://github.com/tweag/nickel/pull/247), check that it correctly cleans the stack when
// evaluating a subequality to `false`.
#[test]
fn poly_eq_nested() {
// Generate an non-empty evaluation context to evaluate equalities over a non-empty stack
let with_context = |t1, t2| {
format!("let not = fun b => if b then true else false in not (not (not (not (({}) == ({})))))", t1, t2)
};
assert_peq!(
with_context(
"{a = 1 + 0; b = 1 + 1; c = 0; d = 0}",
"{ a = 1; b = 3; c = 0; d = 0}"
),
"false"
);
assert_peq!(
with_context(
"[[1,2,3,4], [1,0,3,4], [1,2,3,4], [1,2,3,4]]",
"[[1,2,3,4], [1,2,3,4], [1,2,3,4], [1,2,3,4]]"
),
"false"
);
}
#[test]
fn fields_of() {
assert_peq!("%fieldsOf% {}", "[]");

57
src/stack.rs
View File

@ -10,6 +10,14 @@ use std::rc::Weak;
/// An element of the stack.
#[derive(Debug)]
pub enum Marker {
/// An equality to test.
///
/// When evaluating one equality `t1 == t2`, the abstract machine may generate several new
/// equalities to test (for example, take `t1` and `t2` to be `[1, 2, 3]`). In this case, the
/// first equality is evaluated and the remaining ones - the continuation of the whole
/// computation - are put on the stack as `Eq` elements. If an equality evaluates to `false` at
/// some point, all the consecutive `Eq` elements at the top of the stack are discarded.
Eq(Closure, Closure),
/// An argument of an application.
Arg(Closure, Option<RawSpan>),
/// A thunk, which is pointer to a mutable memory cell to be updated.
@ -26,24 +34,28 @@ impl Marker {
pub fn is_arg(&self) -> bool {
match *self {
Marker::Arg(_, _) => true,
Marker::Thunk(_) => false,
Marker::Cont(_, _, _) => false,
_ => false,
}
}
pub fn is_thunk(&self) -> bool {
match *self {
Marker::Arg(_, _) => false,
Marker::Thunk(_) => true,
Marker::Cont(_, _, _) => false,
_ => false,
}
}
pub fn is_cont(&self) -> bool {
match *self {
Marker::Arg(_, _) => false,
Marker::Thunk(_) => false,
Marker::Cont(_, _, _) => true,
_ => false,
}
}
pub fn is_eq(&self) -> bool {
match *self {
Marker::Eq(..) => true,
_ => false,
}
}
}
@ -99,6 +111,16 @@ impl Stack {
self.0.push(Marker::Cont(cont, len, pos))
}
/// Push a sequence of equalities on the stack.
pub fn push_eqs<I>(&mut self, it: I)
where
I: Iterator<Item = (Closure, Closure)>,
{
self.0.extend(it.map(|(t1, t2)| Marker::Eq(t1, t2)));
}
/// Try to pop an argument from the top of the stack. If `None` is returned, the top element
/// was not an argument and the stack is left unchanged.
pub fn pop_arg(&mut self) -> Option<(Closure, Option<RawSpan>)> {
match self.0.pop() {
Some(Marker::Arg(arg, pos)) => Some((arg, pos)),
@ -110,6 +132,8 @@ impl Stack {
}
}
/// Try to pop a thunk from the top of the stack. If `None` is returned, the top element was
/// not a thunk and the stack is left unchanged.
pub fn pop_thunk(&mut self) -> Option<Weak<RefCell<Closure>>> {
match self.0.pop() {
Some(Marker::Thunk(thunk)) => Some(thunk),
@ -121,6 +145,8 @@ impl Stack {
}
}
/// Try to pop an operator continuation from the top of the stack. If `None` is returned, the
/// top element was not an operator continuation and the stack is left unchanged.
pub fn pop_op_cont(&mut self) -> Option<(OperationCont, usize, Option<RawSpan>)> {
match self.0.pop() {
Some(Marker::Cont(cont, len, pos)) => Some((cont, len, pos)),
@ -132,6 +158,19 @@ impl Stack {
}
}
/// Try to pop an equality from the top of the stack. If `None` is returned, the top element
/// was not an equality and the stack is left unchanged.
pub fn pop_eq(&mut self) -> Option<(Closure, Closure)> {
if self.0.last().map(Marker::is_eq).unwrap_or(false) {
match self.0.pop() {
Some(Marker::Eq(c1, c2)) => Some((c1, c2)),
_ => panic!(),
}
} else {
None
}
}
/// Check if the top element is an argument.
pub fn is_top_thunk(&self) -> bool {
self.0.last().map(Marker::is_thunk).unwrap_or(false)
@ -141,6 +180,12 @@ impl Stack {
pub fn is_top_cont(&self) -> bool {
self.0.last().map(Marker::is_cont).unwrap_or(false)
}
/// Discard all the consecutive equality from the top of the stack. This drops the continuation
/// of the equality being currently evaluated.
pub fn clear_eqs(&mut self) {
while self.pop_eq().is_some() {}
}
}
#[cfg(test)]

15
src/stdlib.rs
View File

@ -1,26 +1,13 @@
//! Load the Nickel standard library in strings at compile-time.
use crate::identifier::Ident;
use crate::term::make as mk_term;
use crate::term::{RichTerm, UnaryOp};
use crate::term::RichTerm;
pub const BUILTINS: &str = include_str!("../stdlib/builtins.ncl");
pub const CONTRACTS: &str = include_str!("../stdlib/contracts.ncl");
pub const LISTS: &str = include_str!("../stdlib/lists.ncl");
pub const RECORDS: &str = include_str!("../stdlib/records.ncl");
/// Accessors to the lists standard library.
pub mod lists {
use super::*;
pub fn all() -> RichTerm {
mk_term::op1(
UnaryOp::StaticAccess(Ident::from("all")),
mk_term::var("lists"),
)
}
}
/// Accessors to the builtin contracts.
pub mod contracts {
use super::*;