diff options
Diffstat (limited to 'dhall/src/core')
-rw-r--r-- | dhall/src/core/thunk.rs | 4 | ||||
-rw-r--r-- | dhall/src/core/value.rs | 19 |
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), + ), } } } |