diff options
Diffstat (limited to '')
-rw-r--r-- | dhall/src/semantics/core/value.rs | 25 | ||||
-rw-r--r-- | dhall/src/semantics/core/value_kind.rs | 82 |
2 files changed, 17 insertions, 90 deletions
diff --git a/dhall/src/semantics/core/value.rs b/dhall/src/semantics/core/value.rs index 7403742..ad0861b 100644 --- a/dhall/src/semantics/core/value.rs +++ b/dhall/src/semantics/core/value.rs @@ -8,6 +8,7 @@ use crate::semantics::error::{TypeError, TypeMessage}; use crate::semantics::phase::normalize::{apply_any, normalize_whnf}; use crate::semantics::phase::typecheck::{builtin_to_value, const_to_value}; use crate::semantics::phase::{NormalizedExpr, Typed}; +use crate::semantics::to_expr; use crate::syntax::{Builtin, Const, Span}; #[derive(Debug, Clone, Copy)] @@ -44,15 +45,6 @@ struct ValueInternal { #[derive(Clone)] pub(crate) struct Value(Rc<RefCell<ValueInternal>>); -#[derive(Copy, Clone)] -/// Controls conversion from `Value` to `Expr` -pub(crate) struct ToExprOptions { - /// Whether to convert all variables to `_` - pub(crate) alpha: bool, - /// Whether to normalize before converting - pub(crate) normalize: bool, -} - impl ValueInternal { fn into_value(self) -> Value { Value(Rc::new(RefCell::new(self))) @@ -174,9 +166,9 @@ impl Value { fn as_internal_mut(&self) -> RefMut<ValueInternal> { self.0.borrow_mut() } - /// WARNING: The returned ValueKind may be entirely unnormalized, in aprticular it may just be an + /// WARNING: The returned ValueKind may be entirely unnormalized, in particular it may just be an /// unevaled PartialExpr. You probably want to use `as_whnf`. - fn as_kind(&self) -> Ref<ValueKind> { + pub(crate) fn as_kind(&self) -> Ref<ValueKind> { Ref::map(self.as_internal(), ValueInternal::as_kind) } /// This is what you want if you want to pattern-match on the value. @@ -187,11 +179,12 @@ impl Value { self.as_kind() } - pub(crate) fn to_expr(&self, opts: ToExprOptions) -> NormalizedExpr { - if opts.normalize { - self.normalize_whnf(); - } - self.as_kind().to_expr(opts) + /// Converts a value back to the corresponding AST expression. + pub(crate) fn to_expr( + &self, + opts: to_expr::ToExprOptions, + ) -> NormalizedExpr { + to_expr::value_to_expr(self, opts) } pub(crate) fn to_whnf_ignore_type(&self) -> ValueKind { self.as_whnf().clone() diff --git a/dhall/src/semantics/core/value_kind.rs b/dhall/src/semantics/core/value_kind.rs index 36ba068..47df39d 100644 --- a/dhall/src/semantics/core/value_kind.rs +++ b/dhall/src/semantics/core/value_kind.rs @@ -1,10 +1,9 @@ use std::collections::HashMap; -use crate::semantics::core::value::{ToExprOptions, Value}; +use crate::semantics::core::value::Value; use crate::semantics::core::var::{AlphaLabel, AlphaVar, Shift, Subst}; -use crate::semantics::phase::typecheck::rc; use crate::semantics::phase::{Normalized, NormalizedExpr}; -use crate::syntax; +use crate::semantics::to_expr; use crate::syntax::{ Builtin, Const, ExprF, Integer, InterpolatedTextContents, Label, NaiveDouble, Natural, @@ -52,77 +51,12 @@ impl ValueKind { Value::from_kind_and_type(self, t) } - pub(crate) fn to_expr(&self, opts: ToExprOptions) -> NormalizedExpr { - match self { - ValueKind::Lam(x, t, e) => rc(ExprF::Lam( - x.to_label_maybe_alpha(opts.alpha), - t.to_expr(opts), - e.to_expr(opts), - )), - 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( - 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)), - 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( - elts.iter().map(|n| n.to_expr(opts)).collect(), - )), - ValueKind::RecordLit(kvs) => rc(ExprF::RecordLit( - kvs.iter() - .map(|(k, v)| (k.clone(), v.to_expr(opts))) - .collect(), - )), - ValueKind::RecordType(kts) => rc(ExprF::RecordType( - kts.iter() - .map(|(k, v)| (k.clone(), v.to_expr(opts))) - .collect(), - )), - ValueKind::UnionType(kts) => rc(ExprF::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::UnionType(kts.clone()).to_expr(opts), - l.clone(), - )), - ValueKind::UnionLit(l, v, kts) => rc(ExprF::App( - ValueKind::UnionConstructor(l.clone(), kts.clone()) - .to_expr(opts), - v.to_expr(opts), - )), - ValueKind::TextLit(elts) => rc(ExprF::TextLit( - elts.iter() - .map(|contents| contents.map_ref(|e| e.to_expr(opts))) - .collect(), - )), - ValueKind::Equivalence(x, y) => rc(ExprF::BinOp( - syntax::BinOp::Equivalence, - x.to_expr(opts), - y.to_expr(opts), - )), - ValueKind::PartialExpr(e) => rc(e.map_ref(|v| v.to_expr(opts))), - } + /// 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) { |