summaryrefslogtreecommitdiff
path: root/dhall/src/semantics
diff options
context:
space:
mode:
Diffstat (limited to 'dhall/src/semantics')
-rw-r--r--dhall/src/semantics/core/value.rs25
-rw-r--r--dhall/src/semantics/core/value_kind.rs82
-rw-r--r--dhall/src/semantics/mod.rs1
-rw-r--r--dhall/src/semantics/phase/mod.rs7
-rw-r--r--dhall/src/semantics/to_expr.rs101
5 files changed, 125 insertions, 91 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) {
diff --git a/dhall/src/semantics/mod.rs b/dhall/src/semantics/mod.rs
index 9d2e462..6438408 100644
--- a/dhall/src/semantics/mod.rs
+++ b/dhall/src/semantics/mod.rs
@@ -1,3 +1,4 @@
pub mod core;
pub mod error;
pub mod phase;
+pub mod to_expr;
diff --git a/dhall/src/semantics/phase/mod.rs b/dhall/src/semantics/phase/mod.rs
index f27088c..6229d15 100644
--- a/dhall/src/semantics/phase/mod.rs
+++ b/dhall/src/semantics/phase/mod.rs
@@ -1,10 +1,11 @@
use std::fmt::Display;
use std::path::Path;
-use crate::semantics::core::value::{ToExprOptions, Value};
+use crate::semantics::core::value::Value;
use crate::semantics::core::value_kind::ValueKind;
use crate::semantics::core::var::{AlphaVar, Shift, Subst};
use crate::semantics::error::{EncodeError, Error, ImportError, TypeError};
+use crate::semantics::to_expr::ToExprOptions;
use crate::syntax::binary;
use crate::syntax::{Builtin, Const, Expr};
use resolve::ImportRoot;
@@ -101,18 +102,22 @@ impl Typed {
Typed::from_const(Const::Type)
}
+ /// Converts a value back to the corresponding AST expression.
pub(crate) fn to_expr(&self) -> NormalizedExpr {
self.0.to_expr(ToExprOptions {
alpha: false,
normalize: false,
})
}
+ /// Converts a value back to the corresponding AST expression, normalizing in the process.
pub fn normalize_to_expr(&self) -> NormalizedExpr {
self.0.to_expr(ToExprOptions {
alpha: false,
normalize: true,
})
}
+ /// Converts a value back to the corresponding AST expression, (akpha,beta)-normalizing in the
+ /// process.
pub(crate) fn normalize_to_expr_alpha(&self) -> NormalizedExpr {
self.0.to_expr(ToExprOptions {
alpha: true,
diff --git a/dhall/src/semantics/to_expr.rs b/dhall/src/semantics/to_expr.rs
new file mode 100644
index 0000000..74bd2fe
--- /dev/null
+++ b/dhall/src/semantics/to_expr.rs
@@ -0,0 +1,101 @@
+use crate::semantics::core::value::Value;
+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};
+
+#[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,
+}
+
+/// Converts a value back to the corresponding AST expression.
+pub(crate) fn value_to_expr(
+ val: &Value,
+ opts: ToExprOptions,
+) -> NormalizedExpr {
+ 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,
+ opts: ToExprOptions,
+) -> NormalizedExpr {
+ match kind {
+ 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))),
+ }
+}
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-23 23:10:47 +0000