diff options
| -rw-r--r-- | dhall/src/semantics/builtins.rs | 67 | ||||
| -rw-r--r-- | dhall/src/semantics/nze/normalize.rs | 52 | ||||
| -rw-r--r-- | dhall/src/semantics/nze/value.rs | 74 |
3 files changed, 110 insertions, 83 deletions
diff --git a/dhall/src/semantics/builtins.rs b/dhall/src/semantics/builtins.rs index 6dbe878..1357adf 100644 --- a/dhall/src/semantics/builtins.rs +++ b/dhall/src/semantics/builtins.rs @@ -1,5 +1,5 @@ use crate::semantics::{ - typecheck, NzEnv, TyExpr, TyExprKind, Value, ValueKind, VarEnv, + self, typecheck, NzEnv, TyExpr, TyExprKind, Value, ValueKind, VarEnv, }; use crate::syntax::map::DupTreeMap; use crate::syntax::Const::Type; @@ -301,14 +301,12 @@ fn apply_builtin( NaturalLit(n) => Ret::ValueKind(IntegerLit(*n as isize)), _ => Ret::DoneAsIs, }, - (NaturalShow, [n]) => { - match &*n.kind() { - NaturalLit(n) => Ret::ValueKind(TextLit(vec![ - InterpolatedTextContents::Text(n.to_string()), - ])), - _ => Ret::DoneAsIs, - } - } + (NaturalShow, [n]) => match &*n.kind() { + NaturalLit(n) => Ret::ValueKind(TextLit( + semantics::TextLit::from_text(n.to_string()), + )), + _ => Ret::DoneAsIs, + }, (NaturalSubtract, [a, b]) => match (&*a.kind(), &*b.kind()) { (NaturalLit(a), NaturalLit(b)) => { Ret::ValueKind(NaturalLit(if b > a { b - a } else { 0 })) @@ -325,7 +323,7 @@ fn apply_builtin( } else { format!("+{}", n) }; - Ret::ValueKind(TextLit(vec![InterpolatedTextContents::Text(s)])) + Ret::ValueKind(TextLit(semantics::TextLit::from_text(s))) } _ => Ret::DoneAsIs, }, @@ -345,42 +343,23 @@ fn apply_builtin( } _ => Ret::DoneAsIs, }, - (DoubleShow, [n]) => { - match &*n.kind() { - DoubleLit(n) => Ret::ValueKind(TextLit(vec![ - InterpolatedTextContents::Text(n.to_string()), - ])), - _ => Ret::DoneAsIs, - } - } + (DoubleShow, [n]) => match &*n.kind() { + DoubleLit(n) => Ret::ValueKind(TextLit( + semantics::TextLit::from_text(n.to_string()), + )), + _ => Ret::DoneAsIs, + }, (TextShow, [v]) => match &*v.kind() { - TextLit(elts) => { - match elts.as_slice() { - // Empty string literal. - [] => { - // Printing InterpolatedText takes care of all the escaping - let txt: InterpolatedText<Normalized> = - std::iter::empty().collect(); - let s = txt.to_string(); - Ret::ValueKind(TextLit(vec![ - InterpolatedTextContents::Text(s), - ])) - } - // If there are no interpolations (invariants ensure that when there are no - // interpolations, there is a single Text item) in the literal. - [InterpolatedTextContents::Text(s)] => { - // Printing InterpolatedText takes care of all the escaping - let txt: InterpolatedText<Normalized> = - std::iter::once(InterpolatedTextContents::Text( - s.clone(), - )) + TextLit(tlit) => { + if let Some(s) = tlit.as_text() { + // Printing InterpolatedText takes care of all the escaping + let txt: InterpolatedText<Normalized> = + std::iter::once(InterpolatedTextContents::Text(s)) .collect(); - let s = txt.to_string(); - Ret::ValueKind(TextLit(vec![ - InterpolatedTextContents::Text(s), - ])) - } - _ => Ret::DoneAsIs, + let s = txt.to_string(); + Ret::ValueKind(TextLit(semantics::TextLit::from_text(s))) + } else { + Ret::DoneAsIs } } _ => Ret::DoneAsIs, 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<InterpolatedTextContents<Value>>); + #[derive(Debug, Clone, PartialEq, Eq)] pub(crate) enum ValueKind { /// Closures @@ -101,9 +109,7 @@ pub(crate) enum ValueKind { UnionConstructor(Label, HashMap<Label, Option<Value>>, Value), // Also keep the type of the uniontype and the constructor around UnionLit(Label, Value, HashMap<Label, Option<Value>>, Value, Value), - // Invariant: in whnf, this must not contain interpolations that are themselves TextLits, and - // contiguous text values must be merged. - TextLit(Vec<InterpolatedTextContents<Value>>), + TextLit(TextLit), Equivalence(Value, Value), // Invariant: in whnf, this must not contain a value captured by one of the variants above. PartialExpr(ExprKind<Value, Normalized>), @@ -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<Item = InterpolatedTextContents<Value>>, + ) -> 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<String> { + 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<Item = &InterpolatedTextContents<Value>> { + 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 { |