diff options
Diffstat (limited to 'dhall')
| -rw-r--r-- | dhall/src/semantics/core/value.rs | 18 | ||||
| -rw-r--r-- | dhall/src/semantics/to_expr.rs | 112 |
2 files changed, 52 insertions, 78 deletions
diff --git a/dhall/src/semantics/core/value.rs b/dhall/src/semantics/core/value.rs index 9b64bd2..f8146f5 100644 --- a/dhall/src/semantics/core/value.rs +++ b/dhall/src/semantics/core/value.rs @@ -306,14 +306,6 @@ impl ValueKind<Value> { Value::from_kind_and_type(self, t) } - /// Converts a value back to the corresponding AST expression. - pub(crate) fn to_expr( - &self, - opts: to_expr::ToExprOptions, - ) -> NormalizedExpr { - to_expr::kind_to_expr(self, opts) - } - pub(crate) fn normalize_mut(&mut self) { match self { ValueKind::Var(_) @@ -390,7 +382,6 @@ impl ValueKind<Value> { } impl<V> ValueKind<V> { - #[allow(dead_code)] pub(crate) fn map_ref_with_special_handling_of_binders<'a, V2>( &'a self, mut map_val: impl FnMut(&'a V) -> V2, @@ -407,6 +398,15 @@ impl<V> ValueKind<V> { .visit(self), ) } + + pub(crate) fn map_ref<'a, V2>( + &'a self, + map_val: impl Fn(&'a V) -> V2, + ) -> ValueKind<V2> { + self.map_ref_with_special_handling_of_binders(&map_val, |_, x| { + map_val(x) + }) + } } /// Compare two values for equality modulo alpha/beta-equivalence. diff --git a/dhall/src/semantics/to_expr.rs b/dhall/src/semantics/to_expr.rs index 9dee7b5..11e289f 100644 --- a/dhall/src/semantics/to_expr.rs +++ b/dhall/src/semantics/to_expr.rs @@ -5,8 +5,8 @@ use crate::semantics::phase::NormalizedExpr; use crate::syntax; use crate::syntax::{Builtin, ExprKind}; -#[derive(Copy, Clone)] /// Controls conversion from `Value` to `Expr` +#[derive(Copy, Clone)] pub(crate) struct ToExprOptions { /// Whether to convert all variables to `_` pub(crate) alpha: bool, @@ -22,84 +22,58 @@ pub(crate) fn value_to_expr( if opts.normalize { val.normalize_whnf(); } - val.as_kind().to_expr(opts) -} -/// Converts a value back to the corresponding AST expression. -pub(crate) fn kind_to_expr( - kind: &ValueKind<Value>, - opts: ToExprOptions, -) -> NormalizedExpr { - match kind { - ValueKind::Lam(x, t, e) => rc(ExprKind::Lam( - x.to_label_maybe_alpha(opts.alpha), - t.to_expr(opts), - e.to_expr(opts), - )), + match val.as_kind().map_ref(|v| value_to_expr(v, opts)) { + ValueKind::Lam(x, t, e) => { + rc(ExprKind::Lam(x.to_label_maybe_alpha(opts.alpha), t, e)) + } ValueKind::AppliedBuiltin(b, args) => args - .iter() - .map(|v| v.to_expr(opts)) - .fold(rc(ExprKind::Builtin(*b)), |acc, v| { - rc(ExprKind::App(acc, v)) - }), - ValueKind::Pi(x, t, e) => rc(ExprKind::Pi( - x.to_label_maybe_alpha(opts.alpha), - t.to_expr(opts), - e.to_expr(opts), - )), + .into_iter() + .fold(rc(ExprKind::Builtin(b)), |acc, v| rc(ExprKind::App(acc, v))), + ValueKind::Pi(x, t, e) => { + rc(ExprKind::Pi(x.to_label_maybe_alpha(opts.alpha), t, e)) + } ValueKind::Var(v) => rc(ExprKind::Var(v.to_var(opts.alpha))), - ValueKind::Const(c) => rc(ExprKind::Const(*c)), - ValueKind::BoolLit(b) => rc(ExprKind::BoolLit(*b)), - ValueKind::NaturalLit(n) => rc(ExprKind::NaturalLit(*n)), - ValueKind::IntegerLit(n) => rc(ExprKind::IntegerLit(*n)), - ValueKind::DoubleLit(n) => rc(ExprKind::DoubleLit(*n)), + ValueKind::Const(c) => rc(ExprKind::Const(c)), + ValueKind::BoolLit(b) => rc(ExprKind::BoolLit(b)), + ValueKind::NaturalLit(n) => rc(ExprKind::NaturalLit(n)), + ValueKind::IntegerLit(n) => rc(ExprKind::IntegerLit(n)), + ValueKind::DoubleLit(n) => rc(ExprKind::DoubleLit(n)), ValueKind::EmptyOptionalLit(n) => rc(ExprKind::App( rc(ExprKind::Builtin(Builtin::OptionalNone)), - n.to_expr(opts), + n, )), - ValueKind::NEOptionalLit(n) => rc(ExprKind::SomeLit(n.to_expr(opts))), - ValueKind::EmptyListLit(n) => { - rc(ExprKind::EmptyListLit(rc(ExprKind::App( - rc(ExprKind::Builtin(Builtin::List)), - n.to_expr(opts), - )))) + ValueKind::NEOptionalLit(n) => rc(ExprKind::SomeLit(n)), + ValueKind::EmptyListLit(n) => rc(ExprKind::EmptyListLit(rc( + ExprKind::App(rc(ExprKind::Builtin(Builtin::List)), n), + ))), + ValueKind::NEListLit(elts) => rc(ExprKind::NEListLit(elts)), + ValueKind::RecordLit(kvs) => { + rc(ExprKind::RecordLit(kvs.into_iter().collect())) + } + ValueKind::RecordType(kts) => { + rc(ExprKind::RecordType(kts.into_iter().collect())) + } + ValueKind::UnionType(kts) => { + rc(ExprKind::UnionType(kts.into_iter().collect())) } - ValueKind::NEListLit(elts) => rc(ExprKind::NEListLit( - elts.iter().map(|n| n.to_expr(opts)).collect(), - )), - ValueKind::RecordLit(kvs) => rc(ExprKind::RecordLit( - kvs.iter() - .map(|(k, v)| (k.clone(), v.to_expr(opts))) - .collect(), - )), - ValueKind::RecordType(kts) => rc(ExprKind::RecordType( - kts.iter() - .map(|(k, v)| (k.clone(), v.to_expr(opts))) - .collect(), - )), - ValueKind::UnionType(kts) => rc(ExprKind::UnionType( - kts.iter() - .map(|(k, v)| (k.clone(), v.as_ref().map(|v| v.to_expr(opts)))) - .collect(), - )), ValueKind::UnionConstructor(l, kts) => rc(ExprKind::Field( - ValueKind::UnionType(kts.clone()).to_expr(opts), - l.clone(), + rc(ExprKind::UnionType(kts.into_iter().collect())), + l, )), ValueKind::UnionLit(l, v, kts) => rc(ExprKind::App( - ValueKind::UnionConstructor(l.clone(), kts.clone()).to_expr(opts), - v.to_expr(opts), - )), - ValueKind::TextLit(elts) => rc(ExprKind::TextLit( - elts.iter() - .map(|contents| contents.map_ref(|e| e.to_expr(opts))) - .collect(), - )), - ValueKind::Equivalence(x, y) => rc(ExprKind::BinOp( - syntax::BinOp::Equivalence, - x.to_expr(opts), - y.to_expr(opts), + rc(ExprKind::Field( + rc(ExprKind::UnionType(kts.into_iter().collect())), + l, + )), + v, )), - ValueKind::PartialExpr(e) => rc(e.map_ref(|v| v.to_expr(opts))), + ValueKind::TextLit(elts) => { + rc(ExprKind::TextLit(elts.into_iter().collect())) + } + ValueKind::Equivalence(x, y) => { + rc(ExprKind::BinOp(syntax::BinOp::Equivalence, x, y)) + } + ValueKind::PartialExpr(e) => rc(e), } } |