diff --git a/src/operation.rs b/src/operation.rs index 34a33a76..698ca7fa 100644 --- a/src/operation.rs +++ b/src/operation.rs @@ -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, clos: Closure, snd_pos: Option, - _stack: &mut Stack, + stack: &mut Stack, pos_op: Option, ) -> Result { 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( - it: T, - env1: &Environment, - env2: &Environment, - env: &mut Environment, - ) -> Term - where - T: Iterator, - { - let subeqs: Vec = 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( + mut it: I, + env: &mut Environment, + env1: Environment, + env2: Environment, + ) -> EqResult + where + I: Iterator, + { + 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::*; diff --git a/src/program.rs b/src/program.rs index e860e798..836c0c09 100644 --- a/src/program.rs +++ b/src/program.rs @@ -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% {}", "[]"); diff --git a/src/stack.rs b/src/stack.rs index 6ebb7ba4..23e8a18b 100644 --- a/src/stack.rs +++ b/src/stack.rs @@ -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), /// 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(&mut self, it: I) + where + I: Iterator, + { + 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)> { 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>> { 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)> { 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)] diff --git a/src/stdlib.rs b/src/stdlib.rs index 5493f95e..6832a35d 100644 --- a/src/stdlib.rs +++ b/src/stdlib.rs @@ -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::*;