summaryrefslogtreecommitdiff
path: root/dhall/src/core
diff options
context:
space:
mode:
authorNadrieril Feneanar2019-08-10 23:15:13 +0200
committerGitHub2019-08-10 23:15:13 +0200
commitb41e0278eda19a495daf0586693f1b5981a89653 (patch)
treecedc8ca740ca0d0bbc74fc987cc0c041f0391b91 /dhall/src/core
parent674fbdc33c788156f76d263b044dccc48c810870 (diff)
parent80c8d87db595c91293af75d710464ac5379c7e28 (diff)
Merge pull request #98 from Nadrieril/catchup-spec
Catchup spec
Diffstat (limited to 'dhall/src/core')
-rw-r--r--dhall/src/core/thunk.rs4
-rw-r--r--dhall/src/core/value.rs19
2 files changed, 22 insertions, 1 deletions
diff --git a/dhall/src/core/thunk.rs b/dhall/src/core/thunk.rs
index 5c569e1..5bc25f2 100644
--- a/dhall/src/core/thunk.rs
+++ b/dhall/src/core/thunk.rs
@@ -221,6 +221,10 @@ impl TypeThunk {
self.0.to_type()
}
+ pub fn to_typed(&self) -> Typed {
+ self.0.clone()
+ }
+
pub fn normalize_to_expr_maybe_alpha(&self, alpha: bool) -> OutputSubExpr {
self.normalize_nf().normalize_to_expr_maybe_alpha(alpha)
}
diff --git a/dhall/src/core/value.rs b/dhall/src/core/value.rs
index d7b9149..26568b5 100644
--- a/dhall/src/core/value.rs
+++ b/dhall/src/core/value.rs
@@ -47,7 +47,7 @@ pub enum Value {
DoubleLit(NaiveDouble),
EmptyOptionalLit(TypeThunk),
NEOptionalLit(Thunk),
- // EmptyListLit(t) means `[] : List t`
+ // EmptyListLit(t) means `[] : List t`, not `[] : t`
EmptyListLit(TypeThunk),
NEListLit(Vec<Thunk>),
RecordLit(HashMap<Label, Thunk>),
@@ -58,6 +58,7 @@ pub enum Value {
// Invariant: this must not contain interpolations that are themselves TextLits, and
// contiguous text values must be merged.
TextLit(Vec<InterpolatedTextContents<Thunk>>),
+ Equivalence(TypeThunk, TypeThunk),
// Invariant: this must not contain a value captured by one of the variants above.
PartialExpr(ExprF<Thunk, X>),
}
@@ -196,6 +197,11 @@ impl Value {
.collect(),
))
}
+ Value::Equivalence(x, y) => rc(ExprF::BinOp(
+ dhall_syntax::BinOp::Equivalence,
+ x.normalize_to_expr_maybe_alpha(alpha),
+ y.normalize_to_expr_maybe_alpha(alpha),
+ )),
Value::PartialExpr(e) => {
rc(e.map_ref_simple(|v| v.normalize_to_expr_maybe_alpha(alpha)))
}
@@ -282,6 +288,10 @@ impl Value {
}
}
}
+ Value::Equivalence(x, y) => {
+ x.normalize_mut();
+ y.normalize_mut();
+ }
Value::PartialExpr(e) => {
// TODO: need map_mut_simple
e.map_ref_simple(|v| {
@@ -418,6 +428,9 @@ impl Shift for Value {
})
.collect::<Result<_, _>>()?,
),
+ Value::Equivalence(x, y) => {
+ Value::Equivalence(x.shift(delta, var)?, y.shift(delta, var)?)
+ }
Value::PartialExpr(e) => Value::PartialExpr(
e.traverse_ref_with_special_handling_of_binders(
|v| Ok(v.shift(delta, var)?),
@@ -533,6 +546,10 @@ impl Subst<Typed> for Value {
})
.collect(),
),
+ Value::Equivalence(x, y) => Value::Equivalence(
+ x.subst_shift(var, val),
+ y.subst_shift(var, val),
+ ),
}
}
}