summaryrefslogtreecommitdiff
path: root/dhall/src/core
diff options
context:
space:
mode:
authorNadrieril Feneanar2019-08-07 23:12:47 +0200
committerGitHub2019-08-07 23:12:47 +0200
commit674fbdc33c788156f76d263b044dccc48c810870 (patch)
tree725eaa49a4f2236d44470279296969b66ba0bbc8 /dhall/src/core
parent8ec422f2319360f986950fcb9aae4bcf65a9c1e2 (diff)
parente81ab9a553bf82f20fa0b0344926258176a21dac (diff)
Merge pull request #95 from Nadrieril/catchup-spec
A lot more catching up on the spec
Diffstat (limited to 'dhall/src/core')
-rw-r--r--dhall/src/core/value.rs23
1 files changed, 8 insertions, 15 deletions
diff --git a/dhall/src/core/value.rs b/dhall/src/core/value.rs
index bc8fa34..d7b9149 100644
--- a/dhall/src/core/value.rs
+++ b/dhall/src/core/value.rs
@@ -47,6 +47,7 @@ pub enum Value {
DoubleLit(NaiveDouble),
EmptyOptionalLit(TypeThunk),
NEOptionalLit(Thunk),
+ // EmptyListLit(t) means `[] : List t`
EmptyListLit(TypeThunk),
NEListLit(Vec<Thunk>),
RecordLit(HashMap<Label, Thunk>),
@@ -128,9 +129,10 @@ impl Value {
Value::NEOptionalLit(n) => {
rc(ExprF::SomeLit(n.normalize_to_expr_maybe_alpha(alpha)))
}
- Value::EmptyListLit(n) => {
- rc(ExprF::EmptyListLit(n.normalize_to_expr_maybe_alpha(alpha)))
- }
+ Value::EmptyListLit(n) => rc(ExprF::EmptyListLit(rc(ExprF::App(
+ rc(ExprF::Builtin(Builtin::List)),
+ n.normalize_to_expr_maybe_alpha(alpha),
+ )))),
Value::NEListLit(elts) => rc(ExprF::NEListLit(
elts.iter()
.map(|n| n.normalize_to_expr_maybe_alpha(alpha))
@@ -176,19 +178,10 @@ impl Value {
.collect();
rc(ExprF::Field(rc(ExprF::UnionType(kts)), l.clone()))
}
- Value::UnionLit(l, v, kts) => rc(ExprF::UnionLit(
- l.clone(),
+ Value::UnionLit(l, v, kts) => rc(ExprF::App(
+ Value::UnionConstructor(l.clone(), kts.clone())
+ .normalize_to_expr_maybe_alpha(alpha),
v.normalize_to_expr_maybe_alpha(alpha),
- kts.iter()
- .map(|(k, v)| {
- (
- k.clone(),
- v.as_ref().map(|v| {
- v.normalize_to_expr_maybe_alpha(alpha)
- }),
- )
- })
- .collect(),
)),
Value::TextLit(elts) => {
use InterpolatedTextContents::{Expr, Text};