summaryrefslogtreecommitdiff
path: root/dhall
diff options
context:
space:
mode:
authorNadrieril2019-04-20 11:02:27 +0200
committerNadrieril2019-04-20 11:02:27 +0200
commita60cf58e5f0cc2f638b788720f9a12cabfdbe3f2 (patch)
tree941152962947608698029598c52696265be6e3e7 /dhall
parent151a14dad84d4d0f02045ea9b69d63e2cb9fe17e (diff)
Text literals
Diffstat (limited to 'dhall')
-rw-r--r--dhall/src/normalize.rs53
1 files changed, 52 insertions, 1 deletions
diff --git a/dhall/src/normalize.rs b/dhall/src/normalize.rs
index b038efd..d006cc5 100644
--- a/dhall/src/normalize.rs
+++ b/dhall/src/normalize.rs
@@ -226,6 +226,7 @@ enum WHNF {
Now,
(NormalizationContext, BTreeMap<Label, Option<InputSubExpr>>),
),
+ TextLit(Vec<InterpolatedTextContents<Now>>),
Expr(OutputSubExpr),
}
@@ -281,6 +282,17 @@ impl WHNF {
})
.collect(),
)),
+ WHNF::TextLit(elts) => rc(ExprF::TextLit(
+ elts.into_iter()
+ .map(|contents| {
+ use InterpolatedTextContents::{Expr, Text};
+ match contents {
+ Expr(n) => Expr(n.normalize().normalize_to_expr()),
+ Text(s) => Text(s),
+ }
+ })
+ .collect(),
+ )),
WHNF::Expr(e) => e,
}
}
@@ -322,6 +334,17 @@ impl WHNF {
.collect(),
),
),
+ WHNF::TextLit(elts) => WHNF::TextLit(
+ elts.into_iter()
+ .map(|contents| {
+ use InterpolatedTextContents::{Expr, Text};
+ match contents {
+ Expr(n) => Expr(n.shift0(delta, label)),
+ Text(s) => Text(s),
+ }
+ })
+ .collect(),
+ ),
}
}
}
@@ -555,6 +578,17 @@ fn reval(ctx: &NormalizationContext, expr: OutputSubExpr) -> WHNF {
ExprF::UnionLit(l, x, kts) => {
WHNF::UnionLit(l, Now::new(ctx.clone(), x), (ctx.clone(), kts))
}
+ ExprF::TextLit(elts) => WHNF::TextLit(
+ elts.into_iter()
+ .map(|contents| {
+ use InterpolatedTextContents::{Expr, Text};
+ match contents {
+ Expr(n) => Expr(Now::new(ctx.clone(), n)),
+ Text(s) => Text(s),
+ }
+ })
+ .collect(),
+ ),
_ => WHNF::Expr(expr),
}
}
@@ -621,6 +655,19 @@ fn normalize_whnf(ctx: &NormalizationContext, expr: InputSubExpr) -> WHNF {
(ctx.clone(), kts.clone()),
)
}
+ ExprF::TextLit(elts) => {
+ return WHNF::TextLit(
+ elts.iter()
+ .map(|contents| {
+ use InterpolatedTextContents::{Expr, Text};
+ match contents {
+ Expr(n) => Expr(Now::new(ctx.clone(), n.clone())),
+ Text(s) => Text(s.clone()),
+ }
+ })
+ .collect(),
+ )
+ }
ExprF::BoolIf(b, e1, e2) => {
let b = normalize_whnf(ctx, b.clone());
match b {
@@ -702,6 +749,10 @@ fn normalize_last_layer(
xs.append(&mut ys);
return WHNF::NEListLit(xs);
}
+ BinOp(TextAppend, WHNF::TextLit(mut x), WHNF::TextLit(mut y)) => {
+ x.append(&mut y);
+ return WHNF::TextLit(x);
+ }
Field(WHNF::UnionType(ctx, kts), l) => {
return WHNF::Closure(Closure::UnionConstructor(ctx, l, kts))
@@ -779,7 +830,7 @@ fn normalize_last_layer(
BinOp(BoolNE, BoolLit(_), BoolLit(_)) => unreachable!(),
BinOp(NaturalPlus, NaturalLit(_), NaturalLit(_)) => unreachable!(),
BinOp(NaturalTimes, NaturalLit(_), NaturalLit(_)) => unreachable!(),
- BinOp(TextAppend, TextLit(x), TextLit(y)) => Done(TextLit(x + y)),
+ BinOp(TextAppend, TextLit(_), TextLit(_)) => unreachable!(),
BinOp(ListAppend, EmptyListLit(_), _) => unreachable!(),
BinOp(ListAppend, _, EmptyListLit(_)) => unreachable!(),
BinOp(ListAppend, NEListLit(_), NEListLit(_)) => unreachable!(),