From dc01ef2030e1177e4f247f4ddc0a3f69241d5cfc Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Thu, 30 Jan 2020 18:32:22 +0000 Subject: Factor out text literals in Value This allows encapsulating invariants properly and reducing clutter --- dhall/src/semantics/nze/normalize.rs | 52 +++++++++++-------------- dhall/src/semantics/nze/value.rs | 74 +++++++++++++++++++++++++++++++----- 2 files changed, 87 insertions(+), 39 deletions(-) (limited to 'dhall/src/semantics/nze') diff --git a/dhall/src/semantics/nze/normalize.rs b/dhall/src/semantics/nze/normalize.rs index 90036e3..89424e9 100644 --- a/dhall/src/semantics/nze/normalize.rs +++ b/dhall/src/semantics/nze/normalize.rs @@ -2,7 +2,8 @@ use std::collections::HashMap; use crate::semantics::NzEnv; use crate::semantics::{ - Binder, BuiltinClosure, Closure, TyExpr, TyExprKind, Value, ValueKind, + Binder, BuiltinClosure, Closure, TextLit, TyExpr, TyExprKind, Value, + ValueKind, }; use crate::syntax::{ BinOp, Builtin, Const, ExprKind, InterpolatedTextContents, @@ -121,7 +122,6 @@ fn apply_binop<'a>( }; use ValueKind::{ BoolLit, EmptyListLit, NEListLit, NaturalLit, RecordLit, RecordType, - TextLit, }; let x_borrow = x.kind(); let y_borrow = y.kind(); @@ -164,25 +164,21 @@ fn apply_binop<'a>( NEListLit(xs.iter().chain(ys.iter()).cloned().collect()), ), - (TextAppend, TextLit(x), _) if x.is_empty() => Ret::ValueRef(y), - (TextAppend, _, TextLit(y)) if y.is_empty() => Ret::ValueRef(x), - (TextAppend, TextLit(x), TextLit(y)) => Ret::ValueKind(TextLit( - squash_textlit(x.iter().chain(y.iter()).cloned()), - )), - (TextAppend, TextLit(x), _) => { - use std::iter::once; - let y = InterpolatedTextContents::Expr(y.clone()); - Ret::ValueKind(TextLit(squash_textlit( - x.iter().cloned().chain(once(y)), - ))) - } - (TextAppend, _, TextLit(y)) => { - use std::iter::once; - let x = InterpolatedTextContents::Expr(x.clone()); - Ret::ValueKind(TextLit(squash_textlit( - once(x).chain(y.iter().cloned()), - ))) + (TextAppend, ValueKind::TextLit(x), _) if x.is_empty() => { + Ret::ValueRef(y) + } + (TextAppend, _, ValueKind::TextLit(y)) if y.is_empty() => { + Ret::ValueRef(x) + } + (TextAppend, ValueKind::TextLit(x), ValueKind::TextLit(y)) => { + Ret::ValueKind(ValueKind::TextLit(x.concat(y))) } + (TextAppend, ValueKind::TextLit(x), _) => Ret::ValueKind( + ValueKind::TextLit(x.concat(&TextLit::interpolate(y.clone()))), + ), + (TextAppend, _, ValueKind::TextLit(y)) => Ret::ValueKind( + ValueKind::TextLit(TextLit::interpolate(x.clone()).concat(y)), + ), (RightBiasedRecordMerge, _, RecordLit(kvs)) if kvs.is_empty() => { Ret::ValueRef(x) @@ -258,8 +254,8 @@ pub(crate) fn normalize_one_layer( ) -> ValueKind { use ValueKind::{ BoolLit, DoubleLit, EmptyOptionalLit, IntegerLit, NEListLit, - NEOptionalLit, NaturalLit, RecordLit, RecordType, TextLit, - UnionConstructor, UnionLit, UnionType, + NEOptionalLit, NaturalLit, RecordLit, RecordType, UnionConstructor, + UnionLit, UnionType, }; let ret = match expr { @@ -309,13 +305,12 @@ pub(crate) fn normalize_one_layer( Ret::ValueKind(UnionType(kvs.into_iter().collect())) } ExprKind::TextLit(elts) => { - use InterpolatedTextContents::Expr; - let elts: Vec<_> = squash_textlit(elts.into_iter()); + let tlit = TextLit::new(elts.into_iter()); // Simplify bare interpolation - if let [Expr(th)] = elts.as_slice() { - Ret::Value(th.clone()) + if let Some(v) = tlit.as_single_expr() { + Ret::Value(v.clone()) } else { - Ret::ValueKind(TextLit(elts)) + Ret::ValueKind(ValueKind::TextLit(tlit)) } } ExprKind::BoolIf(ref b, ref e1, ref e2) => { @@ -455,9 +450,6 @@ pub(crate) fn normalize_whnf(v: ValueKind, ty: &Value) -> ValueKind { ValueKind::AppliedBuiltin(closure) => closure.ensure_whnf(ty), ValueKind::PartialExpr(e) => normalize_one_layer(e, ty, &NzEnv::new()), ValueKind::Thunk(th) => th.eval().kind().clone(), - ValueKind::TextLit(elts) => { - ValueKind::TextLit(squash_textlit(elts.into_iter())) - } // All other cases are already in WHNF v => v, } diff --git a/dhall/src/semantics/nze/value.rs b/dhall/src/semantics/nze/value.rs index 8fad911..06d8df8 100644 --- a/dhall/src/semantics/nze/value.rs +++ b/dhall/src/semantics/nze/value.rs @@ -4,7 +4,9 @@ use std::rc::Rc; use crate::error::{TypeError, TypeMessage}; use crate::semantics::Binder; -use crate::semantics::{apply_any, normalize_tyexpr_whnf, normalize_whnf}; +use crate::semantics::{ + apply_any, normalize_tyexpr_whnf, normalize_whnf, squash_textlit, +}; use crate::semantics::{type_of_builtin, typecheck, TyExpr, TyExprKind}; use crate::semantics::{BuiltinClosure, NzEnv, NzVar, VarEnv}; use crate::syntax::{ @@ -67,6 +69,12 @@ pub(crate) enum Closure { ConstantClosure { env: NzEnv, body: TyExpr }, } +/// A text literal with interpolations. +// Invariant: this must not contain interpolations that are themselves TextLits, and contiguous +// text values must be merged. +#[derive(Debug, Clone, PartialEq, Eq)] +pub(crate) struct TextLit(Vec>); + #[derive(Debug, Clone, PartialEq, Eq)] pub(crate) enum ValueKind { /// Closures @@ -101,9 +109,7 @@ pub(crate) enum ValueKind { UnionConstructor(Label, HashMap>, Value), // Also keep the type of the uniontype and the constructor around UnionLit(Label, Value, HashMap>, Value, Value), - // Invariant: in whnf, this must not contain interpolations that are themselves TextLits, and - // contiguous text values must be merged. - TextLit(Vec>), + TextLit(TextLit), Equivalence(Value, Value), // Invariant: in whnf, this must not contain a value captured by one of the variants above. PartialExpr(ExprKind), @@ -492,11 +498,7 @@ impl ValueKind { x.normalize_mut(); } } - ValueKind::TextLit(elts) => { - for x in elts.iter_mut() { - x.map_mut(Value::normalize_mut); - } - } + ValueKind::TextLit(tlit) => tlit.normalize_mut(), ValueKind::Equivalence(x, y) => { x.normalize_mut(); y.normalize_mut(); @@ -594,6 +596,60 @@ impl Closure { } } +impl TextLit { + pub fn new( + elts: impl Iterator>, + ) -> Self { + TextLit(squash_textlit(elts)) + } + pub fn interpolate(v: Value) -> TextLit { + TextLit(vec![InterpolatedTextContents::Expr(v)]) + } + pub fn from_text(s: String) -> TextLit { + TextLit(vec![InterpolatedTextContents::Text(s)]) + } + + pub fn concat(&self, other: &TextLit) -> TextLit { + TextLit::new(self.iter().chain(other.iter()).cloned()) + } + pub fn is_empty(&self) -> bool { + self.0.is_empty() + } + /// If the literal consists of only one interpolation and not text, return the interpolated + /// value. + pub fn as_single_expr(&self) -> Option<&Value> { + use InterpolatedTextContents::Expr; + if let [Expr(v)] = self.0.as_slice() { + Some(v) + } else { + None + } + } + /// If there are no interpolations, return the corresponding text value. + pub fn as_text(&self) -> Option { + use InterpolatedTextContents::Text; + if self.is_empty() { + Some(String::new()) + } else if let [Text(s)] = self.0.as_slice() { + Some(s.clone()) + } else { + None + } + } + pub fn iter( + &self, + ) -> impl Iterator> { + self.0.iter() + } + /// Normalize the contained values. This does not break the invariant because we have already + /// ensured that no contained values normalize to a TextLit. + pub fn normalize_mut(&mut self) { + for x in self.0.iter_mut() { + x.map_mut(Value::normalize_mut); + } + } +} + /// Compare two values for equality modulo alpha/beta-equivalence. // TODO: use Rc comparison to shortcut on identical pointers impl std::cmp::PartialEq for Value { -- cgit v1.2.3