summaryrefslogtreecommitdiff
path: root/dhall
diff options
context:
space:
mode:
Diffstat (limited to 'dhall')
-rw-r--r--dhall/src/core/value.rs34
-rw-r--r--dhall/src/core/valuef.rs103
-rw-r--r--dhall/src/phase/mod.rs31
3 files changed, 66 insertions, 102 deletions
diff --git a/dhall/src/core/value.rs b/dhall/src/core/value.rs
index 49e30cd..3cccb1d 100644
--- a/dhall/src/core/value.rs
+++ b/dhall/src/core/value.rs
@@ -44,6 +44,15 @@ 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)))
@@ -158,20 +167,12 @@ impl Value {
self.normalize_whnf();
self.as_valuef()
}
- /// WARNING: drop this ref before normalizing the same value or you will run into BorrowMut
- /// panics.
- pub(crate) fn as_nf(&self) -> Ref<ValueF> {
- self.normalize_nf();
- self.as_valuef()
- }
- // TODO: rename `normalize_to_expr`
- pub(crate) fn to_expr(&self) -> NormalizedExpr {
- self.as_whnf().normalize_to_expr()
- }
- // TODO: rename `normalize_to_expr_maybe_alpha`
- pub(crate) fn to_expr_alpha(&self) -> NormalizedExpr {
- self.as_whnf().normalize_to_expr_maybe_alpha(true)
+ pub(crate) fn to_expr(&self, opts: ToExprOptions) -> NormalizedExpr {
+ if opts.normalize {
+ self.normalize_whnf();
+ }
+ self.as_valuef().to_expr(opts)
}
pub(crate) fn to_whnf_ignore_type(&self) -> ValueF {
self.as_whnf().clone()
@@ -223,13 +224,6 @@ impl Value {
}
}
- pub(crate) fn normalize_to_expr_maybe_alpha(
- &self,
- alpha: bool,
- ) -> NormalizedExpr {
- self.as_nf().normalize_to_expr_maybe_alpha(alpha)
- }
-
pub(crate) fn app(&self, v: Value) -> Value {
let body_t = match &*self.get_type_not_sort().as_whnf() {
ValueF::Pi(x, t, e) => {
diff --git a/dhall/src/core/valuef.rs b/dhall/src/core/valuef.rs
index 959f299..7ecec86 100644
--- a/dhall/src/core/valuef.rs
+++ b/dhall/src/core/valuef.rs
@@ -5,7 +5,7 @@ use dhall_syntax::{
NaiveDouble, Natural,
};
-use crate::core::value::Value;
+use crate::core::value::{ToExprOptions, Value};
use crate::core::var::{AlphaLabel, AlphaVar, Shift, Subst};
use crate::phase::{Normalized, NormalizedExpr};
@@ -51,38 +51,23 @@ impl ValueF {
Value::from_valuef_and_type(self, t)
}
- /// Convert the value to a fully normalized syntactic expression
- pub(crate) fn normalize_to_expr(&self) -> NormalizedExpr {
- self.normalize_to_expr_maybe_alpha(false)
- }
- /// Convert the value to a fully normalized syntactic expression. Also alpha-normalize
- /// if alpha is `true`
- pub(crate) fn normalize_to_expr_maybe_alpha(
- &self,
- alpha: bool,
- ) -> NormalizedExpr {
+ pub(crate) fn to_expr(&self, opts: ToExprOptions) -> NormalizedExpr {
match self {
ValueF::Lam(x, t, e) => rc(ExprF::Lam(
- x.to_label_maybe_alpha(alpha),
- t.normalize_to_expr_maybe_alpha(alpha),
- e.normalize_to_expr_maybe_alpha(alpha),
+ x.to_label_maybe_alpha(opts.alpha),
+ t.to_expr(opts),
+ e.to_expr(opts),
)),
- ValueF::AppliedBuiltin(b, args) => {
- let mut e = rc(ExprF::Builtin(*b));
- for v in args {
- e = rc(ExprF::App(
- e,
- v.normalize_to_expr_maybe_alpha(alpha),
- ));
- }
- e
- }
+ ValueF::AppliedBuiltin(b, args) => args
+ .iter()
+ .map(|v| v.to_expr(opts))
+ .fold(rc(ExprF::Builtin(*b)), |acc, v| rc(ExprF::App(acc, v))),
ValueF::Pi(x, t, e) => rc(ExprF::Pi(
- x.to_label_maybe_alpha(alpha),
- t.normalize_to_expr_maybe_alpha(alpha),
- e.normalize_to_expr_maybe_alpha(alpha),
+ x.to_label_maybe_alpha(opts.alpha),
+ t.to_expr(opts),
+ e.to_expr(opts),
)),
- ValueF::Var(v) => rc(ExprF::Var(v.to_var(alpha))),
+ ValueF::Var(v) => rc(ExprF::Var(v.to_var(opts.alpha))),
ValueF::Const(c) => rc(ExprF::Const(*c)),
ValueF::BoolLit(b) => rc(ExprF::BoolLit(*b)),
ValueF::NaturalLit(n) => rc(ExprF::NaturalLit(*n)),
@@ -90,73 +75,47 @@ impl ValueF {
ValueF::DoubleLit(n) => rc(ExprF::DoubleLit(*n)),
ValueF::EmptyOptionalLit(n) => rc(ExprF::App(
rc(ExprF::Builtin(Builtin::OptionalNone)),
- n.normalize_to_expr_maybe_alpha(alpha),
+ n.to_expr(opts),
)),
- ValueF::NEOptionalLit(n) => {
- rc(ExprF::SomeLit(n.normalize_to_expr_maybe_alpha(alpha)))
- }
+ ValueF::NEOptionalLit(n) => rc(ExprF::SomeLit(n.to_expr(opts))),
ValueF::EmptyListLit(n) => rc(ExprF::EmptyListLit(rc(ExprF::App(
rc(ExprF::Builtin(Builtin::List)),
- n.normalize_to_expr_maybe_alpha(alpha),
+ n.to_expr(opts),
)))),
ValueF::NEListLit(elts) => rc(ExprF::NEListLit(
- elts.iter()
- .map(|n| n.normalize_to_expr_maybe_alpha(alpha))
- .collect(),
+ elts.iter().map(|n| n.to_expr(opts)).collect(),
)),
ValueF::RecordLit(kvs) => rc(ExprF::RecordLit(
kvs.iter()
- .map(|(k, v)| {
- (k.clone(), v.normalize_to_expr_maybe_alpha(alpha))
- })
+ .map(|(k, v)| (k.clone(), v.to_expr(opts)))
.collect(),
)),
ValueF::RecordType(kts) => rc(ExprF::RecordType(
kts.iter()
- .map(|(k, v)| {
- (k.clone(), v.normalize_to_expr_maybe_alpha(alpha))
- })
+ .map(|(k, v)| (k.clone(), v.to_expr(opts)))
.collect(),
)),
ValueF::UnionType(kts) => rc(ExprF::UnionType(
kts.iter()
.map(|(k, v)| {
- (
- k.clone(),
- v.as_ref().map(|v| {
- v.normalize_to_expr_maybe_alpha(alpha)
- }),
- )
+ (k.clone(), v.as_ref().map(|v| v.to_expr(opts)))
})
.collect(),
)),
- ValueF::UnionConstructor(l, kts) => {
- let kts = kts
- .iter()
- .map(|(k, v)| {
- (
- k.clone(),
- v.as_ref().map(|v| {
- v.normalize_to_expr_maybe_alpha(alpha)
- }),
- )
- })
- .collect();
- rc(ExprF::Field(rc(ExprF::UnionType(kts)), l.clone()))
- }
+ ValueF::UnionConstructor(l, kts) => rc(ExprF::Field(
+ ValueF::UnionType(kts.clone()).to_expr(opts),
+ l.clone(),
+ )),
ValueF::UnionLit(l, v, kts) => rc(ExprF::App(
- ValueF::UnionConstructor(l.clone(), kts.clone())
- .normalize_to_expr_maybe_alpha(alpha),
- v.normalize_to_expr_maybe_alpha(alpha),
+ ValueF::UnionConstructor(l.clone(), kts.clone()).to_expr(opts),
+ v.to_expr(opts),
)),
ValueF::TextLit(elts) => {
use InterpolatedTextContents::{Expr, Text};
rc(ExprF::TextLit(
elts.iter()
.map(|contents| match contents {
- Expr(e) => {
- Expr(e.normalize_to_expr_maybe_alpha(alpha))
- }
+ Expr(e) => Expr(e.to_expr(opts)),
Text(s) => Text(s.clone()),
})
.collect(),
@@ -164,12 +123,10 @@ impl ValueF {
}
ValueF::Equivalence(x, y) => rc(ExprF::BinOp(
dhall_syntax::BinOp::Equivalence,
- x.normalize_to_expr_maybe_alpha(alpha),
- y.normalize_to_expr_maybe_alpha(alpha),
+ x.to_expr(opts),
+ y.to_expr(opts),
)),
- ValueF::PartialExpr(e) => {
- rc(e.map_ref(|v| v.normalize_to_expr_maybe_alpha(alpha)))
- }
+ ValueF::PartialExpr(e) => rc(e.map_ref(|v| v.to_expr(opts))),
}
}
diff --git a/dhall/src/phase/mod.rs b/dhall/src/phase/mod.rs
index ecc9213..2c5505c 100644
--- a/dhall/src/phase/mod.rs
+++ b/dhall/src/phase/mod.rs
@@ -3,7 +3,7 @@ use std::path::Path;
use dhall_syntax::{Builtin, Const, Expr};
-use crate::core::value::Value;
+use crate::core::value::{ToExprOptions, Value};
use crate::core::valuef::ValueF;
use crate::core::var::{AlphaVar, Shift, Subst};
use crate::error::{EncodeError, Error, ImportError, TypeError};
@@ -71,7 +71,8 @@ impl Resolved {
Ok(typecheck::typecheck(self.0)?.into_typed())
}
pub fn typecheck_with(self, ty: &Typed) -> Result<Typed, TypeError> {
- Ok(typecheck::typecheck_with(self.0, ty.to_expr())?.into_typed())
+ Ok(typecheck::typecheck_with(self.0, ty.normalize_to_expr())?
+ .into_typed())
}
}
@@ -102,11 +103,23 @@ impl Typed {
Typed::from_const(Const::Type)
}
- pub fn to_expr(&self) -> NormalizedExpr {
- self.0.to_expr()
- }
- pub(crate) fn to_expr_alpha(&self) -> NormalizedExpr {
- self.0.to_expr_alpha()
+ pub(crate) fn to_expr(&self) -> NormalizedExpr {
+ self.0.to_expr(ToExprOptions {
+ alpha: false,
+ normalize: false,
+ })
+ }
+ pub fn normalize_to_expr(&self) -> NormalizedExpr {
+ self.0.to_expr(ToExprOptions {
+ alpha: false,
+ normalize: true,
+ })
+ }
+ pub(crate) fn normalize_to_expr_alpha(&self) -> NormalizedExpr {
+ self.0.to_expr(ToExprOptions {
+ alpha: true,
+ normalize: true,
+ })
}
pub(crate) fn to_value(&self) -> Value {
self.0.clone()
@@ -163,10 +176,10 @@ impl Normalized {
}
pub(crate) fn to_expr(&self) -> NormalizedExpr {
- self.0.to_expr()
+ self.0.normalize_to_expr()
}
pub(crate) fn to_expr_alpha(&self) -> NormalizedExpr {
- self.0.to_expr_alpha()
+ self.0.normalize_to_expr_alpha()
}
pub(crate) fn into_typed(self) -> Typed {
self.0
generated by cgit v1.2.3 (git 2.25.1) at 2024-11-09 05:27:56 +0000