summaryrefslogtreecommitdiff
path: root/dhall/src/semantics/nze
diff options
context:
space:
mode:
Diffstat (limited to 'dhall/src/semantics/nze')
-rw-r--r--dhall/src/semantics/nze/normalize.rs52
-rw-r--r--dhall/src/semantics/nze/value.rs74
2 files changed, 87 insertions, 39 deletions
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 {
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-23 18:52:55 +0000