diff options
Diffstat (limited to 'dhall/src/semantics/to_expr.rs')
| -rw-r--r-- | dhall/src/semantics/to_expr.rs | 54 |
1 files changed, 29 insertions, 25 deletions
diff --git a/dhall/src/semantics/to_expr.rs b/dhall/src/semantics/to_expr.rs index 74bd2fe..6099976 100644 --- a/dhall/src/semantics/to_expr.rs +++ b/dhall/src/semantics/to_expr.rs @@ -3,7 +3,7 @@ use crate::semantics::core::value_kind::ValueKind; use crate::semantics::phase::typecheck::rc; use crate::semantics::phase::NormalizedExpr; use crate::syntax; -use crate::syntax::{Builtin, ExprF}; +use crate::syntax::{Builtin, ExprKind}; #[derive(Copy, Clone)] /// Controls conversion from `Value` to `Expr` @@ -31,7 +31,7 @@ pub(crate) fn kind_to_expr( opts: ToExprOptions, ) -> NormalizedExpr { match kind { - ValueKind::Lam(x, t, e) => rc(ExprF::Lam( + ValueKind::Lam(x, t, e) => rc(ExprKind::Lam( x.to_label_maybe_alpha(opts.alpha), t.to_expr(opts), e.to_expr(opts), @@ -39,59 +39,63 @@ pub(crate) fn kind_to_expr( ValueKind::AppliedBuiltin(b, args) => args .iter() .map(|v| v.to_expr(opts)) - .fold(rc(ExprF::Builtin(*b)), |acc, v| rc(ExprF::App(acc, v))), - ValueKind::Pi(x, t, e) => rc(ExprF::Pi( + .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), )), - ValueKind::Var(v) => rc(ExprF::Var(v.to_var(opts.alpha))), - ValueKind::Const(c) => rc(ExprF::Const(*c)), - ValueKind::BoolLit(b) => rc(ExprF::BoolLit(*b)), - ValueKind::NaturalLit(n) => rc(ExprF::NaturalLit(*n)), - ValueKind::IntegerLit(n) => rc(ExprF::IntegerLit(*n)), - ValueKind::DoubleLit(n) => rc(ExprF::DoubleLit(*n)), - ValueKind::EmptyOptionalLit(n) => rc(ExprF::App( - rc(ExprF::Builtin(Builtin::OptionalNone)), + 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::EmptyOptionalLit(n) => rc(ExprKind::App( + rc(ExprKind::Builtin(Builtin::OptionalNone)), n.to_expr(opts), )), - ValueKind::NEOptionalLit(n) => rc(ExprF::SomeLit(n.to_expr(opts))), - ValueKind::EmptyListLit(n) => rc(ExprF::EmptyListLit(rc(ExprF::App( - rc(ExprF::Builtin(Builtin::List)), - n.to_expr(opts), - )))), - ValueKind::NEListLit(elts) => rc(ExprF::NEListLit( + 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::NEListLit(elts) => rc(ExprKind::NEListLit( elts.iter().map(|n| n.to_expr(opts)).collect(), )), - ValueKind::RecordLit(kvs) => rc(ExprF::RecordLit( + ValueKind::RecordLit(kvs) => rc(ExprKind::RecordLit( kvs.iter() .map(|(k, v)| (k.clone(), v.to_expr(opts))) .collect(), )), - ValueKind::RecordType(kts) => rc(ExprF::RecordType( + ValueKind::RecordType(kts) => rc(ExprKind::RecordType( kts.iter() .map(|(k, v)| (k.clone(), v.to_expr(opts))) .collect(), )), - ValueKind::UnionType(kts) => rc(ExprF::UnionType( + 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(ExprF::Field( + ValueKind::UnionConstructor(l, kts) => rc(ExprKind::Field( ValueKind::UnionType(kts.clone()).to_expr(opts), l.clone(), )), - ValueKind::UnionLit(l, v, kts) => rc(ExprF::App( + 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(ExprF::TextLit( + ValueKind::TextLit(elts) => rc(ExprKind::TextLit( elts.iter() .map(|contents| contents.map_ref(|e| e.to_expr(opts))) .collect(), )), - ValueKind::Equivalence(x, y) => rc(ExprF::BinOp( + ValueKind::Equivalence(x, y) => rc(ExprKind::BinOp( syntax::BinOp::Equivalence, x.to_expr(opts), y.to_expr(opts), |