diff options
| -rw-r--r-- | dhall/src/semantics/core/value.rs | 25 | ||||
| -rw-r--r-- | dhall/src/semantics/core/value_kind.rs | 82 | ||||
| -rw-r--r-- | dhall/src/semantics/mod.rs | 1 | ||||
| -rw-r--r-- | dhall/src/semantics/phase/mod.rs | 7 | ||||
| -rw-r--r-- | dhall/src/semantics/to_expr.rs | 101 |
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))), + } +} |