summaryrefslogtreecommitdiff
path: root/dhall/src/semantics/to_expr.rs
diff options
context:
space:
mode:
Diffstat (limited to 'dhall/src/semantics/to_expr.rs')
-rw-r--r--dhall/src/semantics/to_expr.rs23
1 files changed, 3 insertions, 20 deletions
diff --git a/dhall/src/semantics/to_expr.rs b/dhall/src/semantics/to_expr.rs
index 1ece1cc..1adfd49 100644
--- a/dhall/src/semantics/to_expr.rs
+++ b/dhall/src/semantics/to_expr.rs
@@ -1,9 +1,8 @@
-use crate::semantics::core::context::VarCtx;
use crate::semantics::phase::typecheck::rc;
use crate::semantics::phase::NormalizedExpr;
use crate::semantics::{Value, ValueKind};
use crate::syntax;
-use crate::syntax::{Builtin, ExprKind, V};
+use crate::syntax::{Builtin, ExprKind};
/// Controls conversion from `Value` to `Expr`
#[derive(Copy, Clone)]
@@ -16,7 +15,6 @@ pub(crate) struct ToExprOptions {
/// Converts a value back to the corresponding AST expression.
pub(crate) fn value_to_expr(
- ctx: &VarCtx,
val: &Value,
opts: ToExprOptions,
) -> NormalizedExpr {
@@ -25,25 +23,10 @@ pub(crate) fn value_to_expr(
}
let kind = val.as_kind();
- let kind = kind.map_ref_with_special_handling_of_binders(
- |v| value_to_expr(ctx, v, opts),
- |binder, v| value_to_expr(&ctx.insert(binder), v, opts),
- );
+ let kind = kind.map_ref(|v| value_to_expr(v, opts));
match kind {
ValueKind::Var(v) => {
- let b = v.binder();
- let (idx, name) = if opts.alpha {
- (ctx.lookup(&b), "_".into())
- } else {
- (ctx.lookup_by_name(&b), b.name().clone())
- };
- match idx {
- Some(idx) => rc(ExprKind::Var(V(name, idx))),
- None => panic!(
- "internal error: binder {:?} not found in environment",
- b
- ),
- }
+ rc(ExprKind::Var(v.to_var_maybe_alpha(opts.alpha)))
}
ValueKind::Lam(x, t, e) => {
rc(ExprKind::Lam(x.to_label_maybe_alpha(opts.alpha), t, e))