summaryrefslogtreecommitdiff
path: root/dhall/src/semantics/core/value.rs
diff options
context:
space:
mode:
Diffstat (limited to 'dhall/src/semantics/core/value.rs')
-rw-r--r--dhall/src/semantics/core/value.rs25
1 files changed, 9 insertions, 16 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()