summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--dhall/src/semantics/builtins.rs67
-rw-r--r--dhall/src/semantics/nze/normalize.rs52
-rw-r--r--dhall/src/semantics/nze/value.rs74
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 {
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-27 09:43:21 +0000