summaryrefslogtreecommitdiff
path: root/dhall/src/semantics
diff options
context:
space:
mode:
Diffstat (limited to 'dhall/src/semantics')
-rw-r--r--dhall/src/semantics/core/context.rs6
-rw-r--r--dhall/src/semantics/core/mod.rs1
-rw-r--r--dhall/src/semantics/core/value.rs497
-rw-r--r--dhall/src/semantics/core/valuef.rs323
-rw-r--r--dhall/src/semantics/core/var.rs8
-rw-r--r--dhall/src/semantics/error/mod.rs178
-rw-r--r--dhall/src/semantics/mod.rs2
-rw-r--r--dhall/src/semantics/phase/mod.rs30
-rw-r--r--dhall/src/semantics/phase/normalize.rs274
-rw-r--r--dhall/src/semantics/phase/parse.rs2
-rw-r--r--dhall/src/semantics/phase/resolve.rs2
-rw-r--r--dhall/src/semantics/phase/typecheck.rs121
-rw-r--r--dhall/src/semantics/to_expr.rs105
13 files changed, 701 insertions, 848 deletions
diff --git a/dhall/src/semantics/core/context.rs b/dhall/src/semantics/core/context.rs
index d150e56..f755f72 100644
--- a/dhall/src/semantics/core/context.rs
+++ b/dhall/src/semantics/core/context.rs
@@ -1,10 +1,10 @@
use std::collections::HashMap;
use std::rc::Rc;
+use crate::error::TypeError;
use crate::semantics::core::value::Value;
-use crate::semantics::core::valuef::ValueF;
+use crate::semantics::core::value::ValueKind;
use crate::semantics::core::var::{AlphaVar, Shift, Subst};
-use crate::semantics::error::TypeError;
use crate::syntax::{Label, V};
#[derive(Debug, Clone)]
@@ -39,7 +39,7 @@ impl TypecheckContext {
let i = i.under_multiple_binders(&shift_map);
return Some(match i {
CtxItem::Kept(newvar, t) => {
- Value::from_valuef_and_type(ValueF::Var(newvar), t)
+ Value::from_kind_and_type(ValueKind::Var(newvar), t)
}
CtxItem::Replaced(v) => v,
});
diff --git a/dhall/src/semantics/core/mod.rs b/dhall/src/semantics/core/mod.rs
index 08213f7..90d74ea 100644
--- a/dhall/src/semantics/core/mod.rs
+++ b/dhall/src/semantics/core/mod.rs
@@ -1,4 +1,3 @@
pub mod context;
pub mod value;
-pub mod valuef;
pub mod var;
diff --git a/dhall/src/semantics/core/value.rs b/dhall/src/semantics/core/value.rs
index 6e6739f..ca7c4bc 100644
--- a/dhall/src/semantics/core/value.rs
+++ b/dhall/src/semantics/core/value.rs
@@ -1,125 +1,93 @@
use std::cell::{Ref, RefCell, RefMut};
+use std::collections::HashMap;
use std::rc::Rc;
+use crate::error::{TypeError, TypeMessage};
use crate::semantics::core::context::TypecheckContext;
-use crate::semantics::core::valuef::ValueF;
-use crate::semantics::core::var::{AlphaVar, Shift, Subst};
-use crate::semantics::error::{TypeError, TypeMessage};
+use crate::semantics::core::var::{AlphaLabel, AlphaVar, Shift, Subst};
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::syntax::{Builtin, Const, Span};
+use crate::semantics::phase::{Normalized, NormalizedExpr, Typed};
+use crate::semantics::to_expr;
+use crate::syntax::{
+ Builtin, Const, ExprKind, Integer, InterpolatedTextContents, Label,
+ NaiveDouble, Natural, Span,
+};
-#[derive(Debug, Clone, Copy)]
-pub(crate) enum Form {
- /// No constraints; expression may not be normalized at all.
- Unevaled,
- /// Weak Head Normal Form, i.e. normalized up to the first constructor, but subexpressions may
- /// not be normalized. This means that the first constructor of the contained ValueF is the first
- /// constructor of the final Normal Form (NF).
- WHNF,
- /// Normal Form, i.e. completely normalized.
- /// When all the Values in a ValueF are at least in WHNF, and recursively so, then the
- /// ValueF is in NF. This is because WHNF ensures that we have the first constructor of the NF; so
- /// if we have the first constructor of the NF at all levels, we actually have the NF.
- NF,
-}
-use Form::{Unevaled, NF, WHNF};
+use self::Form::{Unevaled, NF, WHNF};
+
+/// Stores a possibly unevaluated value. Gets (partially) normalized on-demand, sharing computation
+/// automatically. Uses a RefCell to share computation.
+/// Can optionally store a type from typechecking to preserve type information.
+/// If you compare for equality two `Value`s in WHNF, then equality will be up to alpha-equivalence
+/// (renaming of bound variables) and beta-equivalence (normalization). It will recursively
+/// normalize as needed.
+#[derive(Clone)]
+pub(crate) struct Value(Rc<RefCell<ValueInternal>>);
-/// Partially normalized value.
/// Invariant: if `form` is `WHNF`, `value` must be in Weak Head Normal Form
/// Invariant: if `form` is `NF`, `value` must be fully normalized
#[derive(Debug)]
struct ValueInternal {
form: Form,
- value: ValueF,
+ kind: ValueKind,
/// This is None if and only if `value` is `Sort` (which doesn't have a type)
ty: Option<Value>,
span: Span,
}
-/// Stores a possibly unevaluated value. Gets (partially) normalized on-demand,
-/// sharing computation automatically. Uses a RefCell to share computation.
-/// Can optionally store a type from typechecking to preserve type information.
-#[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,
+#[derive(Debug, Clone, Copy)]
+pub(crate) enum Form {
+ /// No constraints; expression may not be normalized at all.
+ Unevaled,
+ /// Weak Head Normal Form, i.e. normalized up to the first constructor, but subexpressions may
+ /// not be normalized. This means that the first constructor of the contained ValueKind is the first
+ /// constructor of the final Normal Form (NF).
+ WHNF,
+ /// Normal Form, i.e. completely normalized.
+ /// When all the Values in a ValueKind are at least in WHNF, and recursively so, then the
+ /// ValueKind is in NF. This is because WHNF ensures that we have the first constructor of the NF; so
+ /// if we have the first constructor of the NF at all levels, we actually have the NF.
+ NF,
}
-impl ValueInternal {
- fn into_value(self) -> Value {
- Value(Rc::new(RefCell::new(self)))
- }
- fn as_valuef(&self) -> &ValueF {
- &self.value
- }
-
- fn normalize_whnf(&mut self) {
- take_mut::take_or_recover(
- self,
- // Dummy value in case the other closure panics
- || ValueInternal {
- form: Unevaled,
- value: ValueF::Const(Const::Type),
- ty: None,
- span: Span::Artificial,
- },
- |vint| match (&vint.form, &vint.ty) {
- (Unevaled, Some(ty)) => ValueInternal {
- form: WHNF,
- value: normalize_whnf(vint.value, &ty),
- ty: vint.ty,
- span: vint.span,
- },
- // `value` is `Sort`
- (Unevaled, None) => ValueInternal {
- form: NF,
- value: ValueF::Const(Const::Sort),
- ty: None,
- span: vint.span,
- },
- // Already in WHNF
- (WHNF, _) | (NF, _) => vint,
- },
- )
- }
- fn normalize_nf(&mut self) {
- match self.form {
- Unevaled => {
- self.normalize_whnf();
- self.normalize_nf();
- }
- WHNF => {
- self.value.normalize_mut();
- self.form = NF;
- }
- // Already in NF
- NF => {}
- }
- }
+#[derive(Debug, Clone, PartialEq, Eq)]
+pub(crate) enum ValueKind {
+ /// Closures
+ Lam(AlphaLabel, Value, Value),
+ Pi(AlphaLabel, Value, Value),
+ // Invariant: in whnf, the evaluation must not be able to progress further.
+ AppliedBuiltin(Builtin, Vec<Value>),
- fn get_type(&self) -> Result<&Value, TypeError> {
- match &self.ty {
- Some(t) => Ok(t),
- None => {
- Err(TypeError::new(&TypecheckContext::new(), TypeMessage::Sort))
- }
- }
- }
+ Var(AlphaVar),
+ Const(Const),
+ BoolLit(bool),
+ NaturalLit(Natural),
+ IntegerLit(Integer),
+ DoubleLit(NaiveDouble),
+ EmptyOptionalLit(Value),
+ NEOptionalLit(Value),
+ // EmptyListLit(t) means `[] : List t`, not `[] : t`
+ EmptyListLit(Value),
+ NEListLit(Vec<Value>),
+ RecordType(HashMap<Label, Value>),
+ RecordLit(HashMap<Label, Value>),
+ UnionType(HashMap<Label, Option<Value>>),
+ UnionConstructor(Label, HashMap<Label, Option<Value>>),
+ UnionLit(Label, Value, HashMap<Label, Option<Value>>),
+ // Invariant: in whnf, this must not contain interpolations that are themselves TextLits, and
+ // contiguous text values must be merged.
+ TextLit(Vec<InterpolatedTextContents<Value>>),
+ Equivalence(Value, Value),
+ // Invariant: in whnf, this must not contain a value captured by one of the variants above.
+ PartialExpr(ExprKind<Value, Normalized>),
}
impl Value {
- fn new(value: ValueF, form: Form, ty: Value, span: Span) -> Value {
+ fn new(kind: ValueKind, form: Form, ty: Value, span: Span) -> Value {
ValueInternal {
form,
- value,
+ kind,
ty: Some(ty),
span,
}
@@ -128,23 +96,23 @@ impl Value {
pub(crate) fn const_sort() -> Value {
ValueInternal {
form: NF,
- value: ValueF::Const(Const::Sort),
+ kind: ValueKind::Const(Const::Sort),
ty: None,
span: Span::Artificial,
}
.into_value()
}
- pub(crate) fn from_valuef_and_type(v: ValueF, t: Value) -> Value {
+ pub(crate) fn from_kind_and_type(v: ValueKind, t: Value) -> Value {
Value::new(v, Unevaled, t, Span::Artificial)
}
- pub(crate) fn from_valuef_and_type_and_span(
- v: ValueF,
+ pub(crate) fn from_kind_and_type_and_span(
+ v: ValueKind,
t: Value,
span: Span,
) -> Value {
Value::new(v, Unevaled, t, span)
}
- pub(crate) fn from_valuef_and_type_whnf(v: ValueF, t: Value) -> Value {
+ pub(crate) fn from_kind_and_type_whnf(v: ValueKind, t: Value) -> Value {
Value::new(v, WHNF, t, Span::Artificial)
}
pub(crate) fn from_const(c: Const) -> Self {
@@ -160,7 +128,7 @@ impl Value {
pub(crate) fn as_const(&self) -> Option<Const> {
match &*self.as_whnf() {
- ValueF::Const(c) => Some(*c),
+ ValueKind::Const(c) => Some(*c),
_ => None,
}
}
@@ -174,30 +142,31 @@ impl Value {
fn as_internal_mut(&self) -> RefMut<ValueInternal> {
self.0.borrow_mut()
}
- /// WARNING: The returned ValueF 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_valuef(&self) -> Ref<ValueF> {
- Ref::map(self.as_internal(), ValueInternal::as_valuef)
+ 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.
/// WARNING: drop this ref before normalizing the same value or you will run into BorrowMut
/// panics.
- pub(crate) fn as_whnf(&self) -> Ref<ValueF> {
+ pub(crate) fn as_whnf(&self) -> Ref<ValueKind> {
self.normalize_whnf();
- self.as_valuef()
+ self.as_kind()
}
- 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 {
+ /// 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()
}
/// Before discarding type information, check that it matches the expected return type.
- pub(crate) fn to_whnf_check_type(&self, ty: &Value) -> ValueF {
+ pub(crate) fn to_whnf_check_type(&self, ty: &Value) -> ValueKind {
self.check_type(ty);
self.to_whnf_ignore_type()
}
@@ -234,13 +203,13 @@ impl Value {
pub(crate) fn app(&self, v: Value) -> Value {
let body_t = match &*self.get_type_not_sort().as_whnf() {
- ValueF::Pi(x, t, e) => {
+ ValueKind::Pi(x, t, e) => {
v.check_type(t);
e.subst_shift(&x.into(), &v)
}
_ => unreachable!("Internal type error"),
};
- Value::from_valuef_and_type_whnf(
+ Value::from_kind_and_type_whnf(
apply_any(self.clone(), v, &body_t),
body_t,
)
@@ -265,6 +234,156 @@ impl Value {
}
}
+impl ValueInternal {
+ fn into_value(self) -> Value {
+ Value(Rc::new(RefCell::new(self)))
+ }
+ fn as_kind(&self) -> &ValueKind {
+ &self.kind
+ }
+
+ fn normalize_whnf(&mut self) {
+ take_mut::take_or_recover(
+ self,
+ // Dummy value in case the other closure panics
+ || ValueInternal {
+ form: Unevaled,
+ kind: ValueKind::Const(Const::Type),
+ ty: None,
+ span: Span::Artificial,
+ },
+ |vint| match (&vint.form, &vint.ty) {
+ (Unevaled, Some(ty)) => ValueInternal {
+ form: WHNF,
+ kind: normalize_whnf(vint.kind, &ty),
+ ty: vint.ty,
+ span: vint.span,
+ },
+ // `value` is `Sort`
+ (Unevaled, None) => ValueInternal {
+ form: NF,
+ kind: ValueKind::Const(Const::Sort),
+ ty: None,
+ span: vint.span,
+ },
+ // Already in WHNF
+ (WHNF, _) | (NF, _) => vint,
+ },
+ )
+ }
+ fn normalize_nf(&mut self) {
+ match self.form {
+ Unevaled => {
+ self.normalize_whnf();
+ self.normalize_nf();
+ }
+ WHNF => {
+ self.kind.normalize_mut();
+ self.form = NF;
+ }
+ // Already in NF
+ NF => {}
+ }
+ }
+
+ fn get_type(&self) -> Result<&Value, TypeError> {
+ match &self.ty {
+ Some(t) => Ok(t),
+ None => {
+ Err(TypeError::new(&TypecheckContext::new(), TypeMessage::Sort))
+ }
+ }
+ }
+}
+
+impl ValueKind {
+ pub(crate) fn into_value_with_type(self, t: Value) -> Value {
+ Value::from_kind_and_type(self, t)
+ }
+
+ /// 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) {
+ match self {
+ ValueKind::Var(_)
+ | ValueKind::Const(_)
+ | ValueKind::BoolLit(_)
+ | ValueKind::NaturalLit(_)
+ | ValueKind::IntegerLit(_)
+ | ValueKind::DoubleLit(_) => {}
+
+ ValueKind::EmptyOptionalLit(tth) | ValueKind::EmptyListLit(tth) => {
+ tth.normalize_mut();
+ }
+
+ ValueKind::NEOptionalLit(th) => {
+ th.normalize_mut();
+ }
+ ValueKind::Lam(_, t, e) => {
+ t.normalize_mut();
+ e.normalize_mut();
+ }
+ ValueKind::Pi(_, t, e) => {
+ t.normalize_mut();
+ e.normalize_mut();
+ }
+ ValueKind::AppliedBuiltin(_, args) => {
+ for x in args.iter_mut() {
+ x.normalize_mut();
+ }
+ }
+ ValueKind::NEListLit(elts) => {
+ for x in elts.iter_mut() {
+ x.normalize_mut();
+ }
+ }
+ ValueKind::RecordLit(kvs) => {
+ for x in kvs.values_mut() {
+ x.normalize_mut();
+ }
+ }
+ ValueKind::RecordType(kvs) => {
+ for x in kvs.values_mut() {
+ x.normalize_mut();
+ }
+ }
+ ValueKind::UnionType(kts) | ValueKind::UnionConstructor(_, kts) => {
+ for x in kts.values_mut().flat_map(|opt| opt) {
+ x.normalize_mut();
+ }
+ }
+ ValueKind::UnionLit(_, v, kts) => {
+ v.normalize_mut();
+ for x in kts.values_mut().flat_map(|opt| opt) {
+ x.normalize_mut();
+ }
+ }
+ ValueKind::TextLit(elts) => {
+ for x in elts.iter_mut() {
+ x.map_mut(Value::normalize_mut);
+ }
+ }
+ ValueKind::Equivalence(x, y) => {
+ x.normalize_mut();
+ y.normalize_mut();
+ }
+ ValueKind::PartialExpr(e) => {
+ e.map_mut(Value::normalize_mut);
+ }
+ }
+ }
+
+ pub(crate) fn from_builtin(b: Builtin) -> ValueKind {
+ ValueKind::AppliedBuiltin(b, vec![])
+ }
+}
+
impl Shift for Value {
fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> {
Some(Value(self.0.shift(delta, var)?))
@@ -275,19 +394,84 @@ impl Shift for ValueInternal {
fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> {
Some(ValueInternal {
form: self.form,
- value: self.value.shift(delta, var)?,
+ kind: self.kind.shift(delta, var)?,
ty: self.ty.shift(delta, var)?,
span: self.span.clone(),
})
}
}
+impl Shift for ValueKind {
+ fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> {
+ Some(match self {
+ ValueKind::Lam(x, t, e) => ValueKind::Lam(
+ x.clone(),
+ t.shift(delta, var)?,
+ e.shift(delta, &var.under_binder(x))?,
+ ),
+ ValueKind::AppliedBuiltin(b, args) => {
+ ValueKind::AppliedBuiltin(*b, args.shift(delta, var)?)
+ }
+ ValueKind::Pi(x, t, e) => ValueKind::Pi(
+ x.clone(),
+ t.shift(delta, var)?,
+ e.shift(delta, &var.under_binder(x))?,
+ ),
+ ValueKind::Var(v) => ValueKind::Var(v.shift(delta, var)?),
+ ValueKind::Const(c) => ValueKind::Const(*c),
+ ValueKind::BoolLit(b) => ValueKind::BoolLit(*b),
+ ValueKind::NaturalLit(n) => ValueKind::NaturalLit(*n),
+ ValueKind::IntegerLit(n) => ValueKind::IntegerLit(*n),
+ ValueKind::DoubleLit(n) => ValueKind::DoubleLit(*n),
+ ValueKind::EmptyOptionalLit(tth) => {
+ ValueKind::EmptyOptionalLit(tth.shift(delta, var)?)
+ }
+ ValueKind::NEOptionalLit(th) => {
+ ValueKind::NEOptionalLit(th.shift(delta, var)?)
+ }
+ ValueKind::EmptyListLit(tth) => {
+ ValueKind::EmptyListLit(tth.shift(delta, var)?)
+ }
+ ValueKind::NEListLit(elts) => {
+ ValueKind::NEListLit(elts.shift(delta, var)?)
+ }
+ ValueKind::RecordLit(kvs) => {
+ ValueKind::RecordLit(kvs.shift(delta, var)?)
+ }
+ ValueKind::RecordType(kvs) => {
+ ValueKind::RecordType(kvs.shift(delta, var)?)
+ }
+ ValueKind::UnionType(kts) => {
+ ValueKind::UnionType(kts.shift(delta, var)?)
+ }
+ ValueKind::UnionConstructor(x, kts) => {
+ ValueKind::UnionConstructor(x.clone(), kts.shift(delta, var)?)
+ }
+ ValueKind::UnionLit(x, v, kts) => ValueKind::UnionLit(
+ x.clone(),
+ v.shift(delta, var)?,
+ kts.shift(delta, var)?,
+ ),
+ ValueKind::TextLit(elts) => {
+ ValueKind::TextLit(elts.shift(delta, var)?)
+ }
+ ValueKind::Equivalence(x, y) => ValueKind::Equivalence(
+ x.shift(delta, var)?,
+ y.shift(delta, var)?,
+ ),
+ ValueKind::PartialExpr(e) => {
+ ValueKind::PartialExpr(e.shift(delta, var)?)
+ }
+ })
+ }
+}
+
impl Subst<Value> for Value {
fn subst_shift(&self, var: &AlphaVar, val: &Value) -> Self {
- match &*self.as_valuef() {
+ match &*self.as_kind() {
// If the var matches, we can just reuse the provided value instead of copying it.
// We also check that the types match, if in debug mode.
- ValueF::Var(v) if v == var => {
+ ValueKind::Var(v) if v == var => {
if let Ok(self_ty) = self.get_type() {
val.check_type(&self_ty.subst_shift(var, val));
}
@@ -303,13 +487,80 @@ impl Subst<Value> for ValueInternal {
ValueInternal {
// The resulting value may not stay in wnhf after substitution
form: Unevaled,
- value: self.value.subst_shift(var, val),
+ kind: self.kind.subst_shift(var, val),
ty: self.ty.subst_shift(var, val),
span: self.span.clone(),
}
}
}
+impl Subst<Value> for ValueKind {
+ fn subst_shift(&self, var: &AlphaVar, val: &Value) -> Self {
+ match self {
+ ValueKind::AppliedBuiltin(b, args) => {
+ ValueKind::AppliedBuiltin(*b, args.subst_shift(var, val))
+ }
+ ValueKind::PartialExpr(e) => {
+ ValueKind::PartialExpr(e.subst_shift(var, val))
+ }
+ ValueKind::TextLit(elts) => {
+ ValueKind::TextLit(elts.subst_shift(var, val))
+ }
+ ValueKind::Lam(x, t, e) => ValueKind::Lam(
+ x.clone(),
+ t.subst_shift(var, val),
+ e.subst_shift(&var.under_binder(x), &val.under_binder(x)),
+ ),
+ ValueKind::Pi(x, t, e) => ValueKind::Pi(
+ x.clone(),
+ t.subst_shift(var, val),
+ e.subst_shift(&var.under_binder(x), &val.under_binder(x)),
+ ),
+ ValueKind::Var(v) if v == var => val.to_whnf_ignore_type(),
+ ValueKind::Var(v) => ValueKind::Var(v.shift(-1, var).unwrap()),
+ ValueKind::Const(c) => ValueKind::Const(*c),
+ ValueKind::BoolLit(b) => ValueKind::BoolLit(*b),
+ ValueKind::NaturalLit(n) => ValueKind::NaturalLit(*n),
+ ValueKind::IntegerLit(n) => ValueKind::IntegerLit(*n),
+ ValueKind::DoubleLit(n) => ValueKind::DoubleLit(*n),
+ ValueKind::EmptyOptionalLit(tth) => {
+ ValueKind::EmptyOptionalLit(tth.subst_shift(var, val))
+ }
+ ValueKind::NEOptionalLit(th) => {
+ ValueKind::NEOptionalLit(th.subst_shift(var, val))
+ }
+ ValueKind::EmptyListLit(tth) => {
+ ValueKind::EmptyListLit(tth.subst_shift(var, val))
+ }
+ ValueKind::NEListLit(elts) => {
+ ValueKind::NEListLit(elts.subst_shift(var, val))
+ }
+ ValueKind::RecordLit(kvs) => {
+ ValueKind::RecordLit(kvs.subst_shift(var, val))
+ }
+ ValueKind::RecordType(kvs) => {
+ ValueKind::RecordType(kvs.subst_shift(var, val))
+ }
+ ValueKind::UnionType(kts) => {
+ ValueKind::UnionType(kts.subst_shift(var, val))
+ }
+ ValueKind::UnionConstructor(x, kts) => ValueKind::UnionConstructor(
+ x.clone(),
+ kts.subst_shift(var, val),
+ ),
+ ValueKind::UnionLit(x, v, kts) => ValueKind::UnionLit(
+ x.clone(),
+ v.subst_shift(var, val),
+ kts.subst_shift(var, val),
+ ),
+ ValueKind::Equivalence(x, y) => ValueKind::Equivalence(
+ x.subst_shift(var, val),
+ y.subst_shift(var, val),
+ ),
+ }
+ }
+}
+
// TODO: use Rc comparison to shortcut on identical pointers
impl std::cmp::PartialEq for Value {
fn eq(&self, other: &Self) -> bool {
@@ -321,11 +572,11 @@ impl std::cmp::Eq for Value {}
impl std::fmt::Debug for Value {
fn fmt(&self, fmt: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
let vint: &ValueInternal = &self.as_internal();
- if let ValueF::Const(c) = &vint.value {
+ if let ValueKind::Const(c) = &vint.kind {
write!(fmt, "{:?}", c)
} else {
let mut x = fmt.debug_struct(&format!("Value@{:?}", &vint.form));
- x.field("value", &vint.value);
+ x.field("value", &vint.kind);
if let Some(ty) = vint.ty.as_ref() {
x.field("type", &ty);
} else {
diff --git a/dhall/src/semantics/core/valuef.rs b/dhall/src/semantics/core/valuef.rs
deleted file mode 100644
index 73c715a..0000000
--- a/dhall/src/semantics/core/valuef.rs
+++ /dev/null
@@ -1,323 +0,0 @@
-use std::collections::HashMap;
-
-use crate::semantics::core::value::{ToExprOptions, 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::syntax::{
- Builtin, Const, ExprF, Integer, InterpolatedTextContents, Label,
- NaiveDouble, Natural,
-};
-
-/// A semantic value. Subexpressions are Values, which are partially evaluated expressions that are
-/// normalized on-demand.
-/// If you compare for equality two `ValueF`s in WHNF, then equality will be up to
-/// alpha-equivalence (renaming of bound variables) and beta-equivalence (normalization). It will
-/// recursively normalize as needed.
-#[derive(Debug, Clone, PartialEq, Eq)]
-pub(crate) enum ValueF {
- /// Closures
- Lam(AlphaLabel, Value, Value),
- Pi(AlphaLabel, Value, Value),
- // Invariant: in whnf, the evaluation must not be able to progress further.
- AppliedBuiltin(Builtin, Vec<Value>),
-
- Var(AlphaVar),
- Const(Const),
- BoolLit(bool),
- NaturalLit(Natural),
- IntegerLit(Integer),
- DoubleLit(NaiveDouble),
- EmptyOptionalLit(Value),
- NEOptionalLit(Value),
- // EmptyListLit(t) means `[] : List t`, not `[] : t`
- EmptyListLit(Value),
- NEListLit(Vec<Value>),
- RecordType(HashMap<Label, Value>),
- RecordLit(HashMap<Label, Value>),
- UnionType(HashMap<Label, Option<Value>>),
- UnionConstructor(Label, HashMap<Label, Option<Value>>),
- UnionLit(Label, Value, HashMap<Label, Option<Value>>),
- // Invariant: in whnf, this must not contain interpolations that are themselves TextLits, and
- // contiguous text values must be merged.
- TextLit(Vec<InterpolatedTextContents<Value>>),
- Equivalence(Value, Value),
- // Invariant: in whnf, this must not contain a value captured by one of the variants above.
- PartialExpr(ExprF<Value, Normalized>),
-}
-
-impl ValueF {
- pub(crate) fn into_value_with_type(self, t: Value) -> Value {
- Value::from_valuef_and_type(self, t)
- }
-
- pub(crate) fn to_expr(&self, opts: ToExprOptions) -> NormalizedExpr {
- match self {
- ValueF::Lam(x, t, e) => rc(ExprF::Lam(
- x.to_label_maybe_alpha(opts.alpha),
- t.to_expr(opts),
- e.to_expr(opts),
- )),
- 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(opts.alpha),
- t.to_expr(opts),
- e.to_expr(opts),
- )),
- 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)),
- ValueF::IntegerLit(n) => rc(ExprF::IntegerLit(*n)),
- ValueF::DoubleLit(n) => rc(ExprF::DoubleLit(*n)),
- ValueF::EmptyOptionalLit(n) => rc(ExprF::App(
- rc(ExprF::Builtin(Builtin::OptionalNone)),
- n.to_expr(opts),
- )),
- 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.to_expr(opts),
- )))),
- ValueF::NEListLit(elts) => rc(ExprF::NEListLit(
- elts.iter().map(|n| n.to_expr(opts)).collect(),
- )),
- ValueF::RecordLit(kvs) => rc(ExprF::RecordLit(
- kvs.iter()
- .map(|(k, v)| (k.clone(), v.to_expr(opts)))
- .collect(),
- )),
- ValueF::RecordType(kts) => rc(ExprF::RecordType(
- kts.iter()
- .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.to_expr(opts)))
- })
- .collect(),
- )),
- 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()).to_expr(opts),
- v.to_expr(opts),
- )),
- ValueF::TextLit(elts) => rc(ExprF::TextLit(
- elts.iter()
- .map(|contents| contents.map_ref(|e| e.to_expr(opts)))
- .collect(),
- )),
- ValueF::Equivalence(x, y) => rc(ExprF::BinOp(
- syntax::BinOp::Equivalence,
- x.to_expr(opts),
- y.to_expr(opts),
- )),
- ValueF::PartialExpr(e) => rc(e.map_ref(|v| v.to_expr(opts))),
- }
- }
-
- pub(crate) fn normalize_mut(&mut self) {
- match self {
- ValueF::Var(_)
- | ValueF::Const(_)
- | ValueF::BoolLit(_)
- | ValueF::NaturalLit(_)
- | ValueF::IntegerLit(_)
- | ValueF::DoubleLit(_) => {}
-
- ValueF::EmptyOptionalLit(tth) | ValueF::EmptyListLit(tth) => {
- tth.normalize_mut();
- }
-
- ValueF::NEOptionalLit(th) => {
- th.normalize_mut();
- }
- ValueF::Lam(_, t, e) => {
- t.normalize_mut();
- e.normalize_mut();
- }
- ValueF::Pi(_, t, e) => {
- t.normalize_mut();
- e.normalize_mut();
- }
- ValueF::AppliedBuiltin(_, args) => {
- for x in args.iter_mut() {
- x.normalize_mut();
- }
- }
- ValueF::NEListLit(elts) => {
- for x in elts.iter_mut() {
- x.normalize_mut();
- }
- }
- ValueF::RecordLit(kvs) => {
- for x in kvs.values_mut() {
- x.normalize_mut();
- }
- }
- ValueF::RecordType(kvs) => {
- for x in kvs.values_mut() {
- x.normalize_mut();
- }
- }
- ValueF::UnionType(kts) | ValueF::UnionConstructor(_, kts) => {
- for x in kts.values_mut().flat_map(|opt| opt) {
- x.normalize_mut();
- }
- }
- ValueF::UnionLit(_, v, kts) => {
- v.normalize_mut();
- for x in kts.values_mut().flat_map(|opt| opt) {
- x.normalize_mut();
- }
- }
- ValueF::TextLit(elts) => {
- for x in elts.iter_mut() {
- x.map_mut(Value::normalize_mut);
- }
- }
- ValueF::Equivalence(x, y) => {
- x.normalize_mut();
- y.normalize_mut();
- }
- ValueF::PartialExpr(e) => {
- e.map_mut(Value::normalize_mut);
- }
- }
- }
-
- pub(crate) fn from_builtin(b: Builtin) -> ValueF {
- ValueF::AppliedBuiltin(b, vec![])
- }
-}
-
-impl Shift for ValueF {
- fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> {
- Some(match self {
- ValueF::Lam(x, t, e) => ValueF::Lam(
- x.clone(),
- t.shift(delta, var)?,
- e.shift(delta, &var.under_binder(x))?,
- ),
- ValueF::AppliedBuiltin(b, args) => {
- ValueF::AppliedBuiltin(*b, args.shift(delta, var)?)
- }
- ValueF::Pi(x, t, e) => ValueF::Pi(
- x.clone(),
- t.shift(delta, var)?,
- e.shift(delta, &var.under_binder(x))?,
- ),
- ValueF::Var(v) => ValueF::Var(v.shift(delta, var)?),
- ValueF::Const(c) => ValueF::Const(*c),
- ValueF::BoolLit(b) => ValueF::BoolLit(*b),
- ValueF::NaturalLit(n) => ValueF::NaturalLit(*n),
- ValueF::IntegerLit(n) => ValueF::IntegerLit(*n),
- ValueF::DoubleLit(n) => ValueF::DoubleLit(*n),
- ValueF::EmptyOptionalLit(tth) => {
- ValueF::EmptyOptionalLit(tth.shift(delta, var)?)
- }
- ValueF::NEOptionalLit(th) => {
- ValueF::NEOptionalLit(th.shift(delta, var)?)
- }
- ValueF::EmptyListLit(tth) => {
- ValueF::EmptyListLit(tth.shift(delta, var)?)
- }
- ValueF::NEListLit(elts) => {
- ValueF::NEListLit(elts.shift(delta, var)?)
- }
- ValueF::RecordLit(kvs) => ValueF::RecordLit(kvs.shift(delta, var)?),
- ValueF::RecordType(kvs) => {
- ValueF::RecordType(kvs.shift(delta, var)?)
- }
- ValueF::UnionType(kts) => ValueF::UnionType(kts.shift(delta, var)?),
- ValueF::UnionConstructor(x, kts) => {
- ValueF::UnionConstructor(x.clone(), kts.shift(delta, var)?)
- }
- ValueF::UnionLit(x, v, kts) => ValueF::UnionLit(
- x.clone(),
- v.shift(delta, var)?,
- kts.shift(delta, var)?,
- ),
- ValueF::TextLit(elts) => ValueF::TextLit(elts.shift(delta, var)?),
- ValueF::Equivalence(x, y) => {
- ValueF::Equivalence(x.shift(delta, var)?, y.shift(delta, var)?)
- }
- ValueF::PartialExpr(e) => ValueF::PartialExpr(e.shift(delta, var)?),
- })
- }
-}
-
-impl Subst<Value> for ValueF {
- fn subst_shift(&self, var: &AlphaVar, val: &Value) -> Self {
- match self {
- ValueF::AppliedBuiltin(b, args) => {
- ValueF::AppliedBuiltin(*b, args.subst_shift(var, val))
- }
- ValueF::PartialExpr(e) => {
- ValueF::PartialExpr(e.subst_shift(var, val))
- }
- ValueF::TextLit(elts) => {
- ValueF::TextLit(elts.subst_shift(var, val))
- }
- ValueF::Lam(x, t, e) => ValueF::Lam(
- x.clone(),
- t.subst_shift(var, val),
- e.subst_shift(&var.under_binder(x), &val.under_binder(x)),
- ),
- ValueF::Pi(x, t, e) => ValueF::Pi(
- x.clone(),
- t.subst_shift(var, val),
- e.subst_shift(&var.under_binder(x), &val.under_binder(x)),
- ),
- ValueF::Var(v) if v == var => val.to_whnf_ignore_type(),
- ValueF::Var(v) => ValueF::Var(v.shift(-1, var).unwrap()),
- ValueF::Const(c) => ValueF::Const(*c),
- ValueF::BoolLit(b) => ValueF::BoolLit(*b),
- ValueF::NaturalLit(n) => ValueF::NaturalLit(*n),
- ValueF::IntegerLit(n) => ValueF::IntegerLit(*n),
- ValueF::DoubleLit(n) => ValueF::DoubleLit(*n),
- ValueF::EmptyOptionalLit(tth) => {
- ValueF::EmptyOptionalLit(tth.subst_shift(var, val))
- }
- ValueF::NEOptionalLit(th) => {
- ValueF::NEOptionalLit(th.subst_shift(var, val))
- }
- ValueF::EmptyListLit(tth) => {
- ValueF::EmptyListLit(tth.subst_shift(var, val))
- }
- ValueF::NEListLit(elts) => {
- ValueF::NEListLit(elts.subst_shift(var, val))
- }
- ValueF::RecordLit(kvs) => {
- ValueF::RecordLit(kvs.subst_shift(var, val))
- }
- ValueF::RecordType(kvs) => {
- ValueF::RecordType(kvs.subst_shift(var, val))
- }
- ValueF::UnionType(kts) => {
- ValueF::UnionType(kts.subst_shift(var, val))
- }
- ValueF::UnionConstructor(x, kts) => {
- ValueF::UnionConstructor(x.clone(), kts.subst_shift(var, val))
- }
- ValueF::UnionLit(x, v, kts) => ValueF::UnionLit(
- x.clone(),
- v.subst_shift(var, val),
- kts.subst_shift(var, val),
- ),
- ValueF::Equivalence(x, y) => ValueF::Equivalence(
- x.subst_shift(var, val),
- y.subst_shift(var, val),
- ),
- }
- }
-}
diff --git a/dhall/src/semantics/core/var.rs b/dhall/src/semantics/core/var.rs
index 184a372..1548713 100644
--- a/dhall/src/semantics/core/var.rs
+++ b/dhall/src/semantics/core/var.rs
@@ -1,6 +1,6 @@
use std::collections::HashMap;
-use crate::syntax::{ExprF, InterpolatedTextContents, Label, V};
+use crate::syntax::{ExprKind, InterpolatedTextContents, Label, V};
/// Stores a pair of variables: a normal one and one
/// that corresponds to the alpha-normalized version of the first one.
@@ -12,7 +12,7 @@ pub struct AlphaVar {
}
// Exactly like a Label, but equality returns always true.
-// This is so that ValueF equality is exactly alpha-equivalence.
+// This is so that ValueKind equality is exactly alpha-equivalence.
#[derive(Clone, Eq)]
pub struct AlphaLabel(Label);
@@ -190,7 +190,7 @@ impl<T: Shift> Shift for std::cell::RefCell<T> {
}
}
-impl<T: Shift, E: Clone> Shift for ExprF<T, E> {
+impl<T: Shift, E: Clone> Shift for ExprKind<T, E> {
fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> {
Some(self.traverse_ref_with_special_handling_of_binders(
|v| Ok(v.shift(delta, var)?),
@@ -262,7 +262,7 @@ impl<S, T: Subst<S>> Subst<S> for std::cell::RefCell<T> {
}
}
-impl<S: Shift, T: Subst<S>, E: Clone> Subst<S> for ExprF<T, E> {
+impl<S: Shift, T: Subst<S>, E: Clone> Subst<S> for ExprKind<T, E> {
fn subst_shift(&self, var: &AlphaVar, val: &S) -> Self {
self.map_ref_with_special_handling_of_binders(
|v| v.subst_shift(var, val),
diff --git a/dhall/src/semantics/error/mod.rs b/dhall/src/semantics/error/mod.rs
deleted file mode 100644
index 1288c12..0000000
--- a/dhall/src/semantics/error/mod.rs
+++ /dev/null
@@ -1,178 +0,0 @@
-use std::io::Error as IOError;
-
-use crate::semantics::core::context::TypecheckContext;
-use crate::semantics::core::value::Value;
-use crate::semantics::phase::resolve::ImportStack;
-use crate::semantics::phase::NormalizedExpr;
-use crate::syntax::{BinOp, Import, Label, ParseError, Span};
-
-pub type Result<T> = std::result::Result<T, Error>;
-
-#[derive(Debug)]
-#[non_exhaustive]
-pub enum Error {
- IO(IOError),
- Parse(ParseError),
- Decode(DecodeError),
- Encode(EncodeError),
- Resolve(ImportError),
- Typecheck(TypeError),
-}
-
-#[derive(Debug)]
-pub enum ImportError {
- Recursive(Import<NormalizedExpr>, Box<Error>),
- UnexpectedImport(Import<NormalizedExpr>),
- ImportCycle(ImportStack, Import<NormalizedExpr>),
-}
-
-#[derive(Debug)]
-pub enum DecodeError {
- CBORError(serde_cbor::error::Error),
- WrongFormatError(String),
-}
-
-#[derive(Debug)]
-pub enum EncodeError {
- CBORError(serde_cbor::error::Error),
-}
-
-/// A structured type error that includes context
-#[derive(Debug)]
-pub struct TypeError {
- message: TypeMessage,
- context: TypecheckContext,
-}
-
-/// The specific type error
-#[derive(Debug)]
-pub(crate) enum TypeMessage {
- UnboundVariable(Span),
- InvalidInputType(Value),
- InvalidOutputType(Value),
- NotAFunction(Value),
- TypeMismatch(Value, Value, Value),
- AnnotMismatch(Value, Value),
- InvalidListElement(usize, Value, Value),
- InvalidListType(Value),
- InvalidOptionalType(Value),
- InvalidPredicate(Value),
- IfBranchMismatch(Value, Value),
- IfBranchMustBeTerm(bool, Value),
- InvalidFieldType(Label, Value),
- NotARecord(Label, Value),
- MustCombineRecord(Value),
- MissingRecordField(Label, Value),
- MissingUnionField(Label, Value),
- BinOpTypeMismatch(BinOp, Value),
- InvalidTextInterpolation(Value),
- Merge1ArgMustBeRecord(Value),
- Merge2ArgMustBeUnion(Value),
- MergeEmptyNeedsAnnotation,
- MergeHandlerMissingVariant(Label),
- MergeVariantMissingHandler(Label),
- MergeAnnotMismatch,
- MergeHandlerTypeMismatch,
- MergeHandlerReturnTypeMustNotBeDependent,
- ProjectionMustBeRecord,
- ProjectionMissingEntry,
- Sort,
- RecordTypeDuplicateField,
- RecordTypeMergeRequiresRecordType(Value),
- UnionTypeDuplicateField,
- EquivalenceArgumentMustBeTerm(bool, Value),
- EquivalenceTypeMismatch(Value, Value),
- AssertMismatch(Value, Value),
- AssertMustTakeEquivalence,
-}
-
-impl TypeError {
- pub(crate) fn new(
- context: &TypecheckContext,
- message: TypeMessage,
- ) -> Self {
- TypeError {
- context: context.clone(),
- message,
- }
- }
-}
-
-impl std::fmt::Display for TypeError {
- fn fmt(&self, f: &mut std::fmt::Formatter) -> std::fmt::Result {
- use TypeMessage::*;
- let msg = match &self.message {
- UnboundVariable(span) => span.error("Type error: Unbound variable"),
- InvalidInputType(v) => {
- v.span().error("Type error: Invalid function input")
- }
- InvalidOutputType(v) => {
- v.span().error("Type error: Invalid function output")
- }
- NotAFunction(v) => v.span().error("Type error: Not a function"),
- TypeMismatch(x, y, z) => {
- x.span()
- .error("Type error: Wrong type of function argument")
- + "\n"
- + &z.span().error(format!(
- "This argument has type {:?}",
- z.get_type().unwrap()
- ))
- + "\n"
- + &y.span().error(format!(
- "But the function expected an argument of type {:?}",
- y
- ))
- }
- _ => "Type error: Unhandled error".to_string(),
- };
- write!(f, "{}", msg)
- }
-}
-
-impl std::error::Error for TypeError {}
-
-impl std::fmt::Display for Error {
- fn fmt(&self, f: &mut std::fmt::Formatter) -> std::fmt::Result {
- match self {
- Error::IO(err) => write!(f, "{}", err),
- Error::Parse(err) => write!(f, "{}", err),
- Error::Decode(err) => write!(f, "{:?}", err),
- Error::Encode(err) => write!(f, "{:?}", err),
- Error::Resolve(err) => write!(f, "{:?}", err),
- Error::Typecheck(err) => write!(f, "{}", err),
- }
- }
-}
-
-impl std::error::Error for Error {}
-impl From<IOError> for Error {
- fn from(err: IOError) -> Error {
- Error::IO(err)
- }
-}
-impl From<ParseError> for Error {
- fn from(err: ParseError) -> Error {
- Error::Parse(err)
- }
-}
-impl From<DecodeError> for Error {
- fn from(err: DecodeError) -> Error {
- Error::Decode(err)
- }
-}
-impl From<EncodeError> for Error {
- fn from(err: EncodeError) -> Error {
- Error::Encode(err)
- }
-}
-impl From<ImportError> for Error {
- fn from(err: ImportError) -> Error {
- Error::Resolve(err)
- }
-}
-impl From<TypeError> for Error {
- fn from(err: TypeError) -> Error {
- Error::Typecheck(err)
- }
-}
diff --git a/dhall/src/semantics/mod.rs b/dhall/src/semantics/mod.rs
index 9d2e462..1eeef86 100644
--- a/dhall/src/semantics/mod.rs
+++ b/dhall/src/semantics/mod.rs
@@ -1,3 +1,3 @@
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 752c257..b22120d 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::valuef::ValueF;
+use crate::error::{EncodeError, Error, ImportError, TypeError};
+use crate::semantics::core::value::Value;
+use crate::semantics::core::value::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;
@@ -76,13 +77,6 @@ impl Resolved {
impl Typed {
/// Reduce an expression to its normal form, performing beta reduction
- ///
- /// `normalize` does not type-check the expression. You may want to type-check
- /// expressions before normalizing them since normalization can convert an
- /// ill-typed expression into a well-typed expression.
- ///
- /// However, `normalize` will not fail if the expression is ill-typed and will
- /// leave ill-typed sub-expressions unevaluated.
pub fn normalize(mut self) -> Normalized {
self.normalize_mut();
Normalized(self)
@@ -91,8 +85,8 @@ impl Typed {
pub(crate) fn from_const(c: Const) -> Self {
Typed(Value::from_const(c))
}
- pub(crate) fn from_valuef_and_type(v: ValueF, t: Typed) -> Self {
- Typed(Value::from_valuef_and_type(v, t.into_value()))
+ pub(crate) fn from_kind_and_type(v: ValueKind, t: Typed) -> Self {
+ Typed(Value::from_kind_and_type(v, t.into_value()))
}
pub(crate) fn from_value(th: Value) -> Self {
Typed(th)
@@ -101,18 +95,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, beta-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, (alpha,beta)-normalizing in the
+ /// process.
pub(crate) fn normalize_to_expr_alpha(&self) -> NormalizedExpr {
self.0.to_expr(ToExprOptions {
alpha: true,
@@ -148,8 +146,8 @@ impl Typed {
pub fn make_record_type(
kts: impl Iterator<Item = (String, Typed)>,
) -> Self {
- Typed::from_valuef_and_type(
- ValueF::RecordType(
+ Typed::from_kind_and_type(
+ ValueKind::RecordType(
kts.map(|(k, t)| (k.into(), t.into_value())).collect(),
),
Typed::const_type(),
@@ -158,8 +156,8 @@ impl Typed {
pub fn make_union_type(
kts: impl Iterator<Item = (String, Option<Typed>)>,
) -> Self {
- Typed::from_valuef_and_type(
- ValueF::UnionType(
+ Typed::from_kind_and_type(
+ ValueKind::UnionType(
kts.map(|(k, t)| (k.into(), t.map(|t| t.into_value())))
.collect(),
),
diff --git a/dhall/src/semantics/phase/normalize.rs b/dhall/src/semantics/phase/normalize.rs
index 81c3ce1..d81a910 100644
--- a/dhall/src/semantics/phase/normalize.rs
+++ b/dhall/src/semantics/phase/normalize.rs
@@ -1,14 +1,14 @@
use std::collections::HashMap;
use crate::semantics::core::value::Value;
-use crate::semantics::core::valuef::ValueF;
+use crate::semantics::core::value::ValueKind;
use crate::semantics::core::var::{AlphaLabel, AlphaVar, Shift, Subst};
use crate::semantics::phase::Normalized;
use crate::syntax;
use crate::syntax::Const::Type;
use crate::syntax::{
- BinOp, Builtin, ExprF, InterpolatedText, InterpolatedTextContents, Label,
- NaiveDouble,
+ BinOp, Builtin, ExprKind, InterpolatedText, InterpolatedTextContents,
+ Label, NaiveDouble,
};
// Ad-hoc macro to help construct closures
@@ -19,7 +19,7 @@ macro_rules! make_closure {
Label::from(stringify!($var)).into(),
$n
);
- ValueF::Var(var)
+ ValueKind::Var(var)
.into_value_with_type(make_closure!($($ty)*))
}};
// Warning: assumes that $ty, as a dhall value, has type `Type`
@@ -28,9 +28,9 @@ macro_rules! make_closure {
let ty = make_closure!($($ty)*);
let body = make_closure!($($body)*);
let body_ty = body.get_type_not_sort();
- let lam_ty = ValueF::Pi(var.clone(), ty.clone(), body_ty)
+ let lam_ty = ValueKind::Pi(var.clone(), ty.clone(), body_ty)
.into_value_with_type(Value::from_const(Type));
- ValueF::Lam(var, ty, body).into_value_with_type(lam_ty)
+ ValueKind::Lam(var, ty, body).into_value_with_type(lam_ty)
}};
(Natural) => {
Value::from_builtin(Builtin::Natural)
@@ -43,14 +43,14 @@ macro_rules! make_closure {
let v = make_closure!($($rest)*);
let v_type = v.get_type_not_sort();
let opt_v_type = Value::from_builtin(Builtin::Optional).app(v_type);
- ValueF::NEOptionalLit(v).into_value_with_type(opt_v_type)
+ ValueKind::NEOptionalLit(v).into_value_with_type(opt_v_type)
}};
(1 + $($rest:tt)*) => {
- ValueF::PartialExpr(ExprF::BinOp(
+ ValueKind::PartialExpr(ExprKind::BinOp(
syntax::BinOp::NaturalPlus,
make_closure!($($rest)*),
- Value::from_valuef_and_type(
- ValueF::NaturalLit(1),
+ Value::from_kind_and_type(
+ ValueKind::NaturalLit(1),
make_closure!(Natural)
),
)).into_value_with_type(
@@ -61,9 +61,9 @@ macro_rules! make_closure {
let head = make_closure!($($head)*);
let tail = make_closure!($($tail)*);
let list_type = tail.get_type_not_sort();
- ValueF::PartialExpr(ExprF::BinOp(
+ ValueKind::PartialExpr(ExprKind::BinOp(
syntax::BinOp::ListAppend,
- ValueF::NEListLit(vec![head])
+ ValueKind::NEListLit(vec![head])
.into_value_with_type(list_type.clone()),
tail,
)).into_value_with_type(list_type)
@@ -75,13 +75,13 @@ pub(crate) fn apply_builtin(
b: Builtin,
args: Vec<Value>,
ty: &Value,
-) -> ValueF {
+) -> ValueKind {
use syntax::Builtin::*;
- use ValueF::*;
+ use ValueKind::*;
// Small helper enum
enum Ret<'a> {
- ValueF(ValueF),
+ ValueKind(ValueKind),
Value(Value),
// For applications that can return a function, it's important to keep the remaining
// arguments to apply them to the resulting function.
@@ -90,38 +90,38 @@ pub(crate) fn apply_builtin(
}
let ret = match (b, args.as_slice()) {
- (OptionalNone, [t]) => Ret::ValueF(EmptyOptionalLit(t.clone())),
+ (OptionalNone, [t]) => Ret::ValueKind(EmptyOptionalLit(t.clone())),
(NaturalIsZero, [n]) => match &*n.as_whnf() {
- NaturalLit(n) => Ret::ValueF(BoolLit(*n == 0)),
+ NaturalLit(n) => Ret::ValueKind(BoolLit(*n == 0)),
_ => Ret::DoneAsIs,
},
(NaturalEven, [n]) => match &*n.as_whnf() {
- NaturalLit(n) => Ret::ValueF(BoolLit(*n % 2 == 0)),
+ NaturalLit(n) => Ret::ValueKind(BoolLit(*n % 2 == 0)),
_ => Ret::DoneAsIs,
},
(NaturalOdd, [n]) => match &*n.as_whnf() {
- NaturalLit(n) => Ret::ValueF(BoolLit(*n % 2 != 0)),
+ NaturalLit(n) => Ret::ValueKind(BoolLit(*n % 2 != 0)),
_ => Ret::DoneAsIs,
},
(NaturalToInteger, [n]) => match &*n.as_whnf() {
- NaturalLit(n) => Ret::ValueF(IntegerLit(*n as isize)),
+ NaturalLit(n) => Ret::ValueKind(IntegerLit(*n as isize)),
_ => Ret::DoneAsIs,
},
- (NaturalShow, [n]) => match &*n.as_whnf() {
- NaturalLit(n) => {
- Ret::ValueF(TextLit(vec![InterpolatedTextContents::Text(
- n.to_string(),
- )]))
+ (NaturalShow, [n]) => {
+ match &*n.as_whnf() {
+ NaturalLit(n) => Ret::ValueKind(TextLit(vec![
+ InterpolatedTextContents::Text(n.to_string()),
+ ])),
+ _ => Ret::DoneAsIs,
}
- _ => Ret::DoneAsIs,
- },
+ }
(NaturalSubtract, [a, b]) => match (&*a.as_whnf(), &*b.as_whnf()) {
(NaturalLit(a), NaturalLit(b)) => {
- Ret::ValueF(NaturalLit(if b > a { b - a } else { 0 }))
+ Ret::ValueKind(NaturalLit(if b > a { b - a } else { 0 }))
}
(NaturalLit(0), _) => Ret::Value(b.clone()),
- (_, NaturalLit(0)) => Ret::ValueF(NaturalLit(0)),
- _ if a == b => Ret::ValueF(NaturalLit(0)),
+ (_, NaturalLit(0)) => Ret::ValueKind(NaturalLit(0)),
+ _ if a == b => Ret::ValueKind(NaturalLit(0)),
_ => Ret::DoneAsIs,
},
(IntegerShow, [n]) => match &*n.as_whnf() {
@@ -131,24 +131,24 @@ pub(crate) fn apply_builtin(
} else {
format!("+{}", n)
};
- Ret::ValueF(TextLit(vec![InterpolatedTextContents::Text(s)]))
+ Ret::ValueKind(TextLit(vec![InterpolatedTextContents::Text(s)]))
}
_ => Ret::DoneAsIs,
},
(IntegerToDouble, [n]) => match &*n.as_whnf() {
IntegerLit(n) => {
- Ret::ValueF(DoubleLit(NaiveDouble::from(*n as f64)))
+ Ret::ValueKind(DoubleLit(NaiveDouble::from(*n as f64)))
}
_ => Ret::DoneAsIs,
},
- (DoubleShow, [n]) => match &*n.as_whnf() {
- DoubleLit(n) => {
- Ret::ValueF(TextLit(vec![InterpolatedTextContents::Text(
- n.to_string(),
- )]))
+ (DoubleShow, [n]) => {
+ match &*n.as_whnf() {
+ DoubleLit(n) => Ret::ValueKind(TextLit(vec![
+ InterpolatedTextContents::Text(n.to_string()),
+ ])),
+ _ => Ret::DoneAsIs,
}
- _ => Ret::DoneAsIs,
- },
+ }
(TextShow, [v]) => match &*v.as_whnf() {
TextLit(elts) => {
match elts.as_slice() {
@@ -158,7 +158,7 @@ pub(crate) fn apply_builtin(
let txt: InterpolatedText<Normalized> =
std::iter::empty().collect();
let s = txt.to_string();
- Ret::ValueF(TextLit(vec![
+ Ret::ValueKind(TextLit(vec![
InterpolatedTextContents::Text(s),
]))
}
@@ -172,7 +172,7 @@ pub(crate) fn apply_builtin(
))
.collect();
let s = txt.to_string();
- Ret::ValueF(TextLit(vec![
+ Ret::ValueKind(TextLit(vec![
InterpolatedTextContents::Text(s),
]))
}
@@ -182,28 +182,28 @@ pub(crate) fn apply_builtin(
_ => Ret::DoneAsIs,
},
(ListLength, [_, l]) => match &*l.as_whnf() {
- EmptyListLit(_) => Ret::ValueF(NaturalLit(0)),
- NEListLit(xs) => Ret::ValueF(NaturalLit(xs.len())),
+ EmptyListLit(_) => Ret::ValueKind(NaturalLit(0)),
+ NEListLit(xs) => Ret::ValueKind(NaturalLit(xs.len())),
_ => Ret::DoneAsIs,
},
(ListHead, [_, l]) => match &*l.as_whnf() {
- EmptyListLit(n) => Ret::ValueF(EmptyOptionalLit(n.clone())),
+ EmptyListLit(n) => Ret::ValueKind(EmptyOptionalLit(n.clone())),
NEListLit(xs) => {
- Ret::ValueF(NEOptionalLit(xs.iter().next().unwrap().clone()))
+ Ret::ValueKind(NEOptionalLit(xs.iter().next().unwrap().clone()))
}
_ => Ret::DoneAsIs,
},
(ListLast, [_, l]) => match &*l.as_whnf() {
- EmptyListLit(n) => Ret::ValueF(EmptyOptionalLit(n.clone())),
- NEListLit(xs) => Ret::ValueF(NEOptionalLit(
+ EmptyListLit(n) => Ret::ValueKind(EmptyOptionalLit(n.clone())),
+ NEListLit(xs) => Ret::ValueKind(NEOptionalLit(
xs.iter().rev().next().unwrap().clone(),
)),
_ => Ret::DoneAsIs,
},
(ListReverse, [_, l]) => match &*l.as_whnf() {
- EmptyListLit(n) => Ret::ValueF(EmptyListLit(n.clone())),
+ EmptyListLit(n) => Ret::ValueKind(EmptyListLit(n.clone())),
NEListLit(xs) => {
- Ret::ValueF(NEListLit(xs.iter().rev().cloned().collect()))
+ Ret::ValueKind(NEListLit(xs.iter().rev().cloned().collect()))
}
_ => Ret::DoneAsIs,
},
@@ -222,7 +222,7 @@ pub(crate) fn apply_builtin(
let mut kts = HashMap::new();
kts.insert("index".into(), Value::from_builtin(Natural));
kts.insert("value".into(), t.clone());
- let t = Value::from_valuef_and_type(
+ let t = Value::from_kind_and_type(
RecordType(kts),
Value::from_const(Type),
);
@@ -237,7 +237,7 @@ pub(crate) fn apply_builtin(
let mut kvs = HashMap::new();
kvs.insert(
"index".into(),
- Value::from_valuef_and_type(
+ Value::from_kind_and_type(
NaturalLit(i),
Value::from_builtin(
Builtin::Natural,
@@ -245,7 +245,7 @@ pub(crate) fn apply_builtin(
),
);
kvs.insert("value".into(), e.clone());
- Value::from_valuef_and_type(
+ Value::from_kind_and_type(
RecordLit(kvs),
t.clone(),
)
@@ -254,14 +254,14 @@ pub(crate) fn apply_builtin(
),
_ => unreachable!(),
};
- Ret::ValueF(list)
+ Ret::ValueKind(list)
}
_ => Ret::DoneAsIs,
}
}
(ListBuild, [t, f]) => match &*f.as_whnf() {
// fold/build fusion
- ValueF::AppliedBuiltin(ListFold, args) => {
+ ValueKind::AppliedBuiltin(ListFold, args) => {
if args.len() >= 2 {
Ret::Value(args[1].clone())
} else {
@@ -303,7 +303,7 @@ pub(crate) fn apply_builtin(
},
(OptionalBuild, [t, f]) => match &*f.as_whnf() {
// fold/build fusion
- ValueF::AppliedBuiltin(OptionalFold, args) => {
+ ValueKind::AppliedBuiltin(OptionalFold, args) => {
if args.len() >= 2 {
Ret::Value(args[1].clone())
} else {
@@ -338,7 +338,7 @@ pub(crate) fn apply_builtin(
},
(NaturalBuild, [f]) => match &*f.as_whnf() {
// fold/build fusion
- ValueF::AppliedBuiltin(NaturalFold, args) => {
+ ValueKind::AppliedBuiltin(NaturalFold, args) => {
if !args.is_empty() {
Ret::Value(args[0].clone())
} else {
@@ -375,7 +375,7 @@ pub(crate) fn apply_builtin(
_ => Ret::DoneAsIs,
};
match ret {
- Ret::ValueF(v) => v,
+ Ret::ValueKind(v) => v,
Ret::Value(v) => v.to_whnf_check_type(ty),
Ret::ValueWithRemainingArgs(unconsumed_args, mut v) => {
let n_consumed_args = args.len() - unconsumed_args.len();
@@ -388,23 +388,23 @@ pub(crate) fn apply_builtin(
}
}
-pub(crate) fn apply_any(f: Value, a: Value, ty: &Value) -> ValueF {
+pub(crate) fn apply_any(f: Value, a: Value, ty: &Value) -> ValueKind {
let f_borrow = f.as_whnf();
match &*f_borrow {
- ValueF::Lam(x, _, e) => {
+ ValueKind::Lam(x, _, e) => {
e.subst_shift(&x.into(), &a).to_whnf_check_type(ty)
}
- ValueF::AppliedBuiltin(b, args) => {
+ ValueKind::AppliedBuiltin(b, args) => {
use std::iter::once;
let args = args.iter().cloned().chain(once(a.clone())).collect();
apply_builtin(*b, args, ty)
}
- ValueF::UnionConstructor(l, kts) => {
- ValueF::UnionLit(l.clone(), a, kts.clone())
+ ValueKind::UnionConstructor(l, kts) => {
+ ValueKind::UnionLit(l.clone(), a, kts.clone())
}
_ => {
drop(f_borrow);
- ValueF::PartialExpr(ExprF::App(f, a))
+ ValueKind::PartialExpr(ExprKind::App(f, a))
}
}
}
@@ -426,7 +426,7 @@ pub(crate) fn squash_textlit(
Expr(e) => {
let e_borrow = e.as_whnf();
match &*e_borrow {
- ValueF::TextLit(elts2) => {
+ ValueKind::TextLit(elts2) => {
inner(elts2.iter().cloned(), crnt_str, ret)
}
_ => {
@@ -479,10 +479,10 @@ where
// Small helper enum to avoid repetition
enum Ret<'a> {
- ValueF(ValueF),
+ ValueKind(ValueKind),
Value(Value),
ValueRef(&'a Value),
- Expr(ExprF<Value, Normalized>),
+ Expr(ExprKind<Value, Normalized>),
}
fn apply_binop<'a>(
@@ -496,7 +496,7 @@ fn apply_binop<'a>(
NaturalTimes, RecursiveRecordMerge, RecursiveRecordTypeMerge,
RightBiasedRecordMerge, TextAppend,
};
- use ValueF::{
+ use ValueKind::{
BoolLit, EmptyListLit, NEListLit, NaturalLit, RecordLit, RecordType,
TextLit,
};
@@ -505,58 +505,58 @@ fn apply_binop<'a>(
Some(match (o, &*x_borrow, &*y_borrow) {
(BoolAnd, BoolLit(true), _) => Ret::ValueRef(y),
(BoolAnd, _, BoolLit(true)) => Ret::ValueRef(x),
- (BoolAnd, BoolLit(false), _) => Ret::ValueF(BoolLit(false)),
- (BoolAnd, _, BoolLit(false)) => Ret::ValueF(BoolLit(false)),
+ (BoolAnd, BoolLit(false), _) => Ret::ValueKind(BoolLit(false)),
+ (BoolAnd, _, BoolLit(false)) => Ret::ValueKind(BoolLit(false)),
(BoolAnd, _, _) if x == y => Ret::ValueRef(x),
- (BoolOr, BoolLit(true), _) => Ret::ValueF(BoolLit(true)),
- (BoolOr, _, BoolLit(true)) => Ret::ValueF(BoolLit(true)),
+ (BoolOr, BoolLit(true), _) => Ret::ValueKind(BoolLit(true)),
+ (BoolOr, _, BoolLit(true)) => Ret::ValueKind(BoolLit(true)),
(BoolOr, BoolLit(false), _) => Ret::ValueRef(y),
(BoolOr, _, BoolLit(false)) => Ret::ValueRef(x),
(BoolOr, _, _) if x == y => Ret::ValueRef(x),
(BoolEQ, BoolLit(true), _) => Ret::ValueRef(y),
(BoolEQ, _, BoolLit(true)) => Ret::ValueRef(x),
- (BoolEQ, BoolLit(x), BoolLit(y)) => Ret::ValueF(BoolLit(x == y)),
- (BoolEQ, _, _) if x == y => Ret::ValueF(BoolLit(true)),
+ (BoolEQ, BoolLit(x), BoolLit(y)) => Ret::ValueKind(BoolLit(x == y)),
+ (BoolEQ, _, _) if x == y => Ret::ValueKind(BoolLit(true)),
(BoolNE, BoolLit(false), _) => Ret::ValueRef(y),
(BoolNE, _, BoolLit(false)) => Ret::ValueRef(x),
- (BoolNE, BoolLit(x), BoolLit(y)) => Ret::ValueF(BoolLit(x != y)),
- (BoolNE, _, _) if x == y => Ret::ValueF(BoolLit(false)),
+ (BoolNE, BoolLit(x), BoolLit(y)) => Ret::ValueKind(BoolLit(x != y)),
+ (BoolNE, _, _) if x == y => Ret::ValueKind(BoolLit(false)),
(NaturalPlus, NaturalLit(0), _) => Ret::ValueRef(y),
(NaturalPlus, _, NaturalLit(0)) => Ret::ValueRef(x),
(NaturalPlus, NaturalLit(x), NaturalLit(y)) => {
- Ret::ValueF(NaturalLit(x + y))
+ Ret::ValueKind(NaturalLit(x + y))
}
- (NaturalTimes, NaturalLit(0), _) => Ret::ValueF(NaturalLit(0)),
- (NaturalTimes, _, NaturalLit(0)) => Ret::ValueF(NaturalLit(0)),
+ (NaturalTimes, NaturalLit(0), _) => Ret::ValueKind(NaturalLit(0)),
+ (NaturalTimes, _, NaturalLit(0)) => Ret::ValueKind(NaturalLit(0)),
(NaturalTimes, NaturalLit(1), _) => Ret::ValueRef(y),
(NaturalTimes, _, NaturalLit(1)) => Ret::ValueRef(x),
(NaturalTimes, NaturalLit(x), NaturalLit(y)) => {
- Ret::ValueF(NaturalLit(x * y))
+ Ret::ValueKind(NaturalLit(x * y))
}
(ListAppend, EmptyListLit(_), _) => Ret::ValueRef(y),
(ListAppend, _, EmptyListLit(_)) => Ret::ValueRef(x),
- (ListAppend, NEListLit(xs), NEListLit(ys)) => Ret::ValueF(NEListLit(
- xs.iter().chain(ys.iter()).cloned().collect(),
- )),
+ (ListAppend, NEListLit(xs), NEListLit(ys)) => Ret::ValueKind(
+ NEListLit(xs.iter().chain(ys.iter()).cloned().collect()),
+ ),
(TextAppend, TextLit(x), _) if x.is_empty() => Ret::ValueRef(y),
(TextAppend, _, TextLit(y)) if y.is_empty() => Ret::ValueRef(x),
- (TextAppend, TextLit(x), TextLit(y)) => Ret::ValueF(TextLit(
+ (TextAppend, TextLit(x), TextLit(y)) => Ret::ValueKind(TextLit(
squash_textlit(x.iter().chain(y.iter()).cloned()),
)),
(TextAppend, TextLit(x), _) => {
use std::iter::once;
let y = InterpolatedTextContents::Expr(y.clone());
- Ret::ValueF(TextLit(squash_textlit(
+ Ret::ValueKind(TextLit(squash_textlit(
x.iter().cloned().chain(once(y)),
)))
}
(TextAppend, _, TextLit(y)) => {
use std::iter::once;
let x = InterpolatedTextContents::Expr(x.clone());
- Ret::ValueF(TextLit(squash_textlit(
+ Ret::ValueKind(TextLit(squash_textlit(
once(x).chain(y.iter().cloned()),
)))
}
@@ -573,7 +573,7 @@ fn apply_binop<'a>(
// Insert only if key not already present
kvs.entry(x.clone()).or_insert_with(|| v.clone());
}
- Ret::ValueF(RecordLit(kvs))
+ Ret::ValueKind(RecordLit(kvs))
}
(RecursiveRecordMerge, _, RecordLit(kvs)) if kvs.is_empty() => {
@@ -589,8 +589,8 @@ fn apply_binop<'a>(
_ => unreachable!("Internal type error"),
};
let kvs = merge_maps::<_, _, _, !>(kvs1, kvs2, |k, v1, v2| {
- Ok(Value::from_valuef_and_type(
- ValueF::PartialExpr(ExprF::BinOp(
+ Ok(Value::from_kind_and_type(
+ ValueKind::PartialExpr(ExprKind::BinOp(
RecursiveRecordMerge,
v1.clone(),
v2.clone(),
@@ -598,7 +598,7 @@ fn apply_binop<'a>(
kts.get(k).expect("Internal type error").clone(),
))
})?;
- Ret::ValueF(RecordLit(kvs))
+ Ret::ValueKind(RecordLit(kvs))
}
(RecursiveRecordTypeMerge, _, _) | (Equivalence, _, _) => {
@@ -610,46 +610,46 @@ fn apply_binop<'a>(
}
pub(crate) fn normalize_one_layer(
- expr: ExprF<Value, Normalized>,
+ expr: ExprKind<Value, Normalized>,
ty: &Value,
-) -> ValueF {
- use ValueF::{
+) -> ValueKind {
+ use ValueKind::{
AppliedBuiltin, BoolLit, DoubleLit, EmptyListLit, IntegerLit,
NEListLit, NEOptionalLit, NaturalLit, RecordLit, TextLit,
UnionConstructor, UnionLit, UnionType,
};
let ret = match expr {
- ExprF::Import(_) => unreachable!(
+ ExprKind::Import(_) => unreachable!(
"There should remain no imports in a resolved expression"
),
// Those cases have already been completely handled in the typechecking phase (using
// `RetWhole`), so they won't appear here.
- ExprF::Lam(_, _, _)
- | ExprF::Pi(_, _, _)
- | ExprF::Let(_, _, _, _)
- | ExprF::Embed(_)
- | ExprF::Const(_)
- | ExprF::Builtin(_)
- | ExprF::Var(_)
- | ExprF::Annot(_, _)
- | ExprF::RecordType(_)
- | ExprF::UnionType(_) => {
+ ExprKind::Lam(_, _, _)
+ | ExprKind::Pi(_, _, _)
+ | ExprKind::Let(_, _, _, _)
+ | ExprKind::Embed(_)
+ | ExprKind::Const(_)
+ | ExprKind::Builtin(_)
+ | ExprKind::Var(_)
+ | ExprKind::Annot(_, _)
+ | ExprKind::RecordType(_)
+ | ExprKind::UnionType(_) => {
unreachable!("This case should have been handled in typecheck")
}
- ExprF::Assert(_) => Ret::Expr(expr),
- ExprF::App(v, a) => Ret::Value(v.app(a)),
- ExprF::BoolLit(b) => Ret::ValueF(BoolLit(b)),
- ExprF::NaturalLit(n) => Ret::ValueF(NaturalLit(n)),
- ExprF::IntegerLit(n) => Ret::ValueF(IntegerLit(n)),
- ExprF::DoubleLit(n) => Ret::ValueF(DoubleLit(n)),
- ExprF::SomeLit(e) => Ret::ValueF(NEOptionalLit(e)),
- ExprF::EmptyListLit(ref t) => {
+ ExprKind::Assert(_) => Ret::Expr(expr),
+ ExprKind::App(v, a) => Ret::Value(v.app(a)),
+ ExprKind::BoolLit(b) => Ret::ValueKind(BoolLit(b)),
+ ExprKind::NaturalLit(n) => Ret::ValueKind(NaturalLit(n)),
+ ExprKind::IntegerLit(n) => Ret::ValueKind(IntegerLit(n)),
+ ExprKind::DoubleLit(n) => Ret::ValueKind(DoubleLit(n)),
+ ExprKind::SomeLit(e) => Ret::ValueKind(NEOptionalLit(e)),
+ ExprKind::EmptyListLit(ref t) => {
// Check if the type is of the form `List x`
let t_borrow = t.as_whnf();
match &*t_borrow {
AppliedBuiltin(Builtin::List, args) if args.len() == 1 => {
- Ret::ValueF(EmptyListLit(args[0].clone()))
+ Ret::ValueKind(EmptyListLit(args[0].clone()))
}
_ => {
drop(t_borrow);
@@ -657,23 +657,23 @@ pub(crate) fn normalize_one_layer(
}
}
}
- ExprF::NEListLit(elts) => {
- Ret::ValueF(NEListLit(elts.into_iter().collect()))
+ ExprKind::NEListLit(elts) => {
+ Ret::ValueKind(NEListLit(elts.into_iter().collect()))
}
- ExprF::RecordLit(kvs) => {
- Ret::ValueF(RecordLit(kvs.into_iter().collect()))
+ ExprKind::RecordLit(kvs) => {
+ Ret::ValueKind(RecordLit(kvs.into_iter().collect()))
}
- ExprF::TextLit(elts) => {
+ ExprKind::TextLit(elts) => {
use InterpolatedTextContents::Expr;
let elts: Vec<_> = squash_textlit(elts.into_iter());
// Simplify bare interpolation
if let [Expr(th)] = elts.as_slice() {
Ret::Value(th.clone())
} else {
- Ret::ValueF(TextLit(elts))
+ Ret::ValueKind(TextLit(elts))
}
}
- ExprF::BoolIf(ref b, ref e1, ref e2) => {
+ ExprKind::BoolIf(ref b, ref e1, ref e2) => {
let b_borrow = b.as_whnf();
match &*b_borrow {
BoolLit(true) => Ret::ValueRef(e1),
@@ -695,18 +695,18 @@ pub(crate) fn normalize_one_layer(
}
}
}
- ExprF::BinOp(o, ref x, ref y) => match apply_binop(o, x, y, ty) {
+ ExprKind::BinOp(o, ref x, ref y) => match apply_binop(o, x, y, ty) {
Some(ret) => ret,
None => Ret::Expr(expr),
},
- ExprF::Projection(_, ref ls) if ls.is_empty() => {
- Ret::ValueF(RecordLit(HashMap::new()))
+ ExprKind::Projection(_, ref ls) if ls.is_empty() => {
+ Ret::ValueKind(RecordLit(HashMap::new()))
}
- ExprF::Projection(ref v, ref ls) => {
+ ExprKind::Projection(ref v, ref ls) => {
let v_borrow = v.as_whnf();
match &*v_borrow {
- RecordLit(kvs) => Ret::ValueF(RecordLit(
+ RecordLit(kvs) => Ret::ValueKind(RecordLit(
ls.iter()
.filter_map(|l| {
kvs.get(l).map(|x| (l.clone(), x.clone()))
@@ -719,7 +719,7 @@ pub(crate) fn normalize_one_layer(
}
}
}
- ExprF::Field(ref v, ref l) => {
+ ExprKind::Field(ref v, ref l) => {
let v_borrow = v.as_whnf();
match &*v_borrow {
RecordLit(kvs) => match kvs.get(l) {
@@ -730,7 +730,7 @@ pub(crate) fn normalize_one_layer(
}
},
UnionType(kts) => {
- Ret::ValueF(UnionConstructor(l.clone(), kts.clone()))
+ Ret::ValueKind(UnionConstructor(l.clone(), kts.clone()))
}
_ => {
drop(v_borrow);
@@ -738,11 +738,11 @@ pub(crate) fn normalize_one_layer(
}
}
}
- ExprF::ProjectionByExpr(_, _) => {
+ ExprKind::ProjectionByExpr(_, _) => {
unimplemented!("selection by expression")
}
- ExprF::Merge(ref handlers, ref variant, _) => {
+ ExprKind::Merge(ref handlers, ref variant, _) => {
let handlers_borrow = handlers.as_whnf();
let variant_borrow = variant.as_whnf();
match (&*handlers_borrow, &*variant_borrow) {
@@ -769,24 +769,24 @@ pub(crate) fn normalize_one_layer(
}
}
}
- ExprF::ToMap(_, _) => unimplemented!("toMap"),
+ ExprKind::ToMap(_, _) => unimplemented!("toMap"),
};
match ret {
- Ret::ValueF(v) => v,
+ Ret::ValueKind(v) => v,
Ret::Value(v) => v.to_whnf_check_type(ty),
Ret::ValueRef(v) => v.to_whnf_check_type(ty),
- Ret::Expr(expr) => ValueF::PartialExpr(expr),
+ Ret::Expr(expr) => ValueKind::PartialExpr(expr),
}
}
-/// Normalize a ValueF into WHNF
-pub(crate) fn normalize_whnf(v: ValueF, ty: &Value) -> ValueF {
+/// Normalize a ValueKind into WHNF
+pub(crate) fn normalize_whnf(v: ValueKind, ty: &Value) -> ValueKind {
match v {
- ValueF::AppliedBuiltin(b, args) => apply_builtin(b, args, ty),
- ValueF::PartialExpr(e) => normalize_one_layer(e, ty),
- ValueF::TextLit(elts) => {
- ValueF::TextLit(squash_textlit(elts.into_iter()))
+ ValueKind::AppliedBuiltin(b, args) => apply_builtin(b, args, ty),
+ ValueKind::PartialExpr(e) => normalize_one_layer(e, ty),
+ ValueKind::TextLit(elts) => {
+ ValueKind::TextLit(squash_textlit(elts.into_iter()))
}
// All other cases are already in WHNF
v => v,
diff --git a/dhall/src/semantics/phase/parse.rs b/dhall/src/semantics/phase/parse.rs
index 4c8ad7b..00db422 100644
--- a/dhall/src/semantics/phase/parse.rs
+++ b/dhall/src/semantics/phase/parse.rs
@@ -2,7 +2,7 @@ use std::fs::File;
use std::io::Read;
use std::path::Path;
-use crate::semantics::error::Error;
+use crate::error::Error;
use crate::semantics::phase::resolve::ImportRoot;
use crate::semantics::phase::Parsed;
use crate::syntax::binary;
diff --git a/dhall/src/semantics/phase/resolve.rs b/dhall/src/semantics/phase/resolve.rs
index 86dc7ae..cc4a024 100644
--- a/dhall/src/semantics/phase/resolve.rs
+++ b/dhall/src/semantics/phase/resolve.rs
@@ -1,7 +1,7 @@
use std::collections::HashMap;
use std::path::{Path, PathBuf};
-use crate::semantics::error::{Error, ImportError};
+use crate::error::{Error, ImportError};
use crate::semantics::phase::{Normalized, NormalizedExpr, Parsed, Resolved};
use crate::syntax;
use crate::syntax::{FilePath, ImportLocation, URL};
diff --git a/dhall/src/semantics/phase/typecheck.rs b/dhall/src/semantics/phase/typecheck.rs
index 59380a3..c439f74 100644
--- a/dhall/src/semantics/phase/typecheck.rs
+++ b/dhall/src/semantics/phase/typecheck.rs
@@ -1,16 +1,17 @@
use std::cmp::max;
use std::collections::HashMap;
+use crate::error::{TypeError, TypeMessage};
use crate::semantics::core::context::TypecheckContext;
use crate::semantics::core::value::Value;
-use crate::semantics::core::valuef::ValueF;
+use crate::semantics::core::value::ValueKind;
use crate::semantics::core::var::{Shift, Subst};
-use crate::semantics::error::{TypeError, TypeMessage};
use crate::semantics::phase::normalize::merge_maps;
use crate::semantics::phase::Normalized;
use crate::syntax;
use crate::syntax::{
- Builtin, Const, Expr, ExprF, InterpolatedTextContents, Label, RawExpr, Span,
+ Builtin, Const, Expr, ExprKind, InterpolatedTextContents, Label, Span,
+ UnspannedExpr,
};
fn tck_pi_type(
@@ -39,8 +40,8 @@ fn tck_pi_type(
let k = function_check(ka, kb);
- Ok(Value::from_valuef_and_type(
- ValueF::Pi(x.into(), tx, te),
+ Ok(Value::from_kind_and_type(
+ ValueKind::Pi(x.into(), tx, te),
Value::from_const(k),
))
}
@@ -71,8 +72,8 @@ fn tck_record_type(
};
}
- Ok(Value::from_valuef_and_type(
- ValueF::RecordType(new_kts),
+ Ok(Value::from_kind_and_type(
+ ValueKind::RecordType(new_kts),
Value::from_const(k),
))
}
@@ -116,8 +117,8 @@ where
// an union type with only unary variants also has type Type
let k = k.unwrap_or(Const::Type);
- Ok(Value::from_valuef_and_type(
- ValueF::UnionType(new_kts),
+ Ok(Value::from_kind_and_type(
+ ValueKind::UnionType(new_kts),
Value::from_const(k),
))
}
@@ -131,42 +132,42 @@ fn function_check(a: Const, b: Const) -> Const {
}
pub(crate) fn const_to_value(c: Const) -> Value {
- let v = ValueF::Const(c);
+ let v = ValueKind::Const(c);
match c {
Const::Type => {
- Value::from_valuef_and_type(v, const_to_value(Const::Kind))
+ Value::from_kind_and_type(v, const_to_value(Const::Kind))
}
Const::Kind => {
- Value::from_valuef_and_type(v, const_to_value(Const::Sort))
+ Value::from_kind_and_type(v, const_to_value(Const::Sort))
}
Const::Sort => Value::const_sort(),
}
}
-pub fn rc<E>(x: RawExpr<E>) -> Expr<E> {
+pub fn rc<E>(x: UnspannedExpr<E>) -> Expr<E> {
Expr::new(x, Span::Artificial)
}
// Ad-hoc macro to help construct the types of builtins
macro_rules! make_type {
- (Type) => { ExprF::Const(Const::Type) };
- (Bool) => { ExprF::Builtin(Builtin::Bool) };
- (Natural) => { ExprF::Builtin(Builtin::Natural) };
- (Integer) => { ExprF::Builtin(Builtin::Integer) };
- (Double) => { ExprF::Builtin(Builtin::Double) };
- (Text) => { ExprF::Builtin(Builtin::Text) };
+ (Type) => { ExprKind::Const(Const::Type) };
+ (Bool) => { ExprKind::Builtin(Builtin::Bool) };
+ (Natural) => { ExprKind::Builtin(Builtin::Natural) };
+ (Integer) => { ExprKind::Builtin(Builtin::Integer) };
+ (Double) => { ExprKind::Builtin(Builtin::Double) };
+ (Text) => { ExprKind::Builtin(Builtin::Text) };
($var:ident) => {
- ExprF::Var(syntax::V(stringify!($var).into(), 0))
+ ExprKind::Var(syntax::V(stringify!($var).into(), 0))
};
(Optional $ty:ident) => {
- ExprF::App(
- rc(ExprF::Builtin(Builtin::Optional)),
+ ExprKind::App(
+ rc(ExprKind::Builtin(Builtin::Optional)),
rc(make_type!($ty))
)
};
(List $($rest:tt)*) => {
- ExprF::App(
- rc(ExprF::Builtin(Builtin::List)),
+ ExprKind::App(
+ rc(ExprKind::Builtin(Builtin::List)),
rc(make_type!($($rest)*))
)
};
@@ -178,24 +179,24 @@ macro_rules! make_type {
rc(make_type!($ty)),
);
)*
- ExprF::RecordType(kts)
+ ExprKind::RecordType(kts)
}};
($ty:ident -> $($rest:tt)*) => {
- ExprF::Pi(
+ ExprKind::Pi(
"_".into(),
rc(make_type!($ty)),
rc(make_type!($($rest)*))
)
};
(($($arg:tt)*) -> $($rest:tt)*) => {
- ExprF::Pi(
+ ExprKind::Pi(
"_".into(),
rc(make_type!($($arg)*)),
rc(make_type!($($rest)*))
)
};
(forall ($var:ident : $($ty:tt)*) -> $($rest:tt)*) => {
- ExprF::Pi(
+ ExprKind::Pi(
stringify!($var).into(),
rc(make_type!($($ty)*)),
rc(make_type!($($rest)*))
@@ -290,8 +291,8 @@ fn type_of_builtin<E>(b: Builtin) -> Expr<E> {
pub(crate) fn builtin_to_value(b: Builtin) -> Value {
let ctx = TypecheckContext::new();
- Value::from_valuef_and_type(
- ValueF::from_builtin(b),
+ Value::from_kind_and_type(
+ ValueKind::from_builtin(b),
type_with(&ctx, type_of_builtin(b)).unwrap(),
)
}
@@ -304,7 +305,7 @@ fn type_with(
ctx: &TypecheckContext,
e: Expr<Normalized>,
) -> Result<Value, TypeError> {
- use syntax::ExprF::{Annot, Embed, Lam, Let, Pi, Var};
+ use syntax::ExprKind::{Annot, Embed, Lam, Let, Pi, Var};
let span = e.span();
Ok(match e.as_ref() {
@@ -313,8 +314,8 @@ fn type_with(
let ctx2 = ctx.insert_type(var, annot.clone());
let body = type_with(&ctx2, body.clone())?;
let body_type = body.get_type()?;
- Value::from_valuef_and_type(
- ValueF::Lam(var.clone().into(), annot.clone(), body),
+ Value::from_kind_and_type(
+ ValueKind::Lam(var.clone().into(), annot.clone(), body),
tck_pi_type(ctx, var.clone(), annot, body_type)?,
)
}
@@ -359,13 +360,13 @@ fn type_with(
/// layer.
fn type_last_layer(
ctx: &TypecheckContext,
- e: ExprF<Value, Normalized>,
+ e: ExprKind<Value, Normalized>,
span: Span,
) -> Result<Value, TypeError> {
use syntax::BinOp::*;
use syntax::Builtin::*;
use syntax::Const::Type;
- use syntax::ExprF::*;
+ use syntax::ExprKind::*;
use TypeMessage::*;
let mkerr = |msg: TypeMessage| Err(TypeError::new(ctx, msg));
@@ -389,7 +390,7 @@ fn type_last_layer(
let tf = f.get_type()?;
let tf_borrow = tf.as_whnf();
let (x, tx, tb) = match &*tf_borrow {
- ValueF::Pi(x, tx, tb) => (x, tx, tb),
+ ValueKind::Pi(x, tx, tb) => (x, tx, tb),
_ => return mkerr(NotAFunction(f.clone())),
};
if &a.get_type()? != tx {
@@ -406,8 +407,8 @@ fn type_last_layer(
}
Assert(t) => {
match &*t.as_whnf() {
- ValueF::Equivalence(x, y) if x == y => {}
- ValueF::Equivalence(x, y) => {
+ ValueKind::Equivalence(x, y) if x == y => {}
+ ValueKind::Equivalence(x, y) => {
return mkerr(AssertMismatch(x.clone(), y.clone()))
}
_ => return mkerr(AssertMustTakeEquivalence),
@@ -415,7 +416,7 @@ fn type_last_layer(
RetTypeOnly(t.clone())
}
BoolIf(x, y, z) => {
- if *x.get_type()?.as_whnf() != ValueF::from_builtin(Bool) {
+ if *x.get_type()?.as_whnf() != ValueKind::from_builtin(Bool) {
return mkerr(InvalidPredicate(x.clone()));
}
@@ -435,7 +436,7 @@ fn type_last_layer(
}
EmptyListLit(t) => {
match &*t.as_whnf() {
- ValueF::AppliedBuiltin(syntax::Builtin::List, args)
+ ValueKind::AppliedBuiltin(syntax::Builtin::List, args)
if args.len() == 1 => {}
_ => return mkerr(InvalidListType(t.clone())),
}
@@ -482,7 +483,7 @@ fn type_last_layer(
)?),
Field(r, x) => {
match &*r.get_type()?.as_whnf() {
- ValueF::RecordType(kts) => match kts.get(&x) {
+ ValueKind::RecordType(kts) => match kts.get(&x) {
Some(tth) => {
RetTypeOnly(tth.clone())
},
@@ -492,7 +493,7 @@ fn type_last_layer(
// TODO: branch here only when r.get_type() is a Const
_ => {
match &*r.as_whnf() {
- ValueF::UnionType(kts) => match kts.get(&x) {
+ ValueKind::UnionType(kts) => match kts.get(&x) {
// Constructor has type T -> < x: T, ... >
Some(Some(t)) => {
RetTypeOnly(
@@ -553,14 +554,14 @@ fn type_last_layer(
// Extract the LHS record type
let l_type_borrow = l_type.as_whnf();
let kts_x = match &*l_type_borrow {
- ValueF::RecordType(kts) => kts,
+ ValueKind::RecordType(kts) => kts,
_ => return mkerr(MustCombineRecord(l.clone())),
};
// Extract the RHS record type
let r_type_borrow = r_type.as_whnf();
let kts_y = match &*r_type_borrow {
- ValueF::RecordType(kts) => kts,
+ ValueKind::RecordType(kts) => kts,
_ => return mkerr(MustCombineRecord(r.clone())),
};
@@ -578,7 +579,7 @@ fn type_last_layer(
}
BinOp(RecursiveRecordMerge, l, r) => RetTypeOnly(type_last_layer(
ctx,
- ExprF::BinOp(
+ ExprKind::BinOp(
RecursiveRecordTypeMerge,
l.get_type()?,
r.get_type()?,
@@ -589,7 +590,7 @@ fn type_last_layer(
// Extract the LHS record type
let borrow_l = l.as_whnf();
let kts_x = match &*borrow_l {
- ValueF::RecordType(kts) => kts,
+ ValueKind::RecordType(kts) => kts,
_ => {
return mkerr(RecordTypeMergeRequiresRecordType(l.clone()))
}
@@ -598,7 +599,7 @@ fn type_last_layer(
// Extract the RHS record type
let borrow_r = r.as_whnf();
let kts_y = match &*borrow_r {
- ValueF::RecordType(kts) => kts,
+ ValueKind::RecordType(kts) => kts,
_ => {
return mkerr(RecordTypeMergeRequiresRecordType(r.clone()))
}
@@ -612,7 +613,7 @@ fn type_last_layer(
|_, l: &Value, r: &Value| {
type_last_layer(
ctx,
- ExprF::BinOp(
+ ExprKind::BinOp(
RecursiveRecordTypeMerge,
l.clone(),
r.clone(),
@@ -626,7 +627,7 @@ fn type_last_layer(
}
BinOp(o @ ListAppend, l, r) => {
match &*l.get_type()?.as_whnf() {
- ValueF::AppliedBuiltin(List, _) => {}
+ ValueKind::AppliedBuiltin(List, _) => {}
_ => return mkerr(BinOpTypeMismatch(*o, l.clone())),
}
@@ -648,8 +649,8 @@ fn type_last_layer(
return mkerr(EquivalenceTypeMismatch(r.clone(), l.clone()));
}
- RetWhole(Value::from_valuef_and_type(
- ValueF::Equivalence(l.clone(), r.clone()),
+ RetWhole(Value::from_kind_and_type(
+ ValueKind::Equivalence(l.clone(), r.clone()),
Value::from_const(Type),
))
}
@@ -684,14 +685,14 @@ fn type_last_layer(
let record_type = record.get_type()?;
let record_borrow = record_type.as_whnf();
let handlers = match &*record_borrow {
- ValueF::RecordType(kts) => kts,
+ ValueKind::RecordType(kts) => kts,
_ => return mkerr(Merge1ArgMustBeRecord(record.clone())),
};
let union_type = union.get_type()?;
let union_borrow = union_type.as_whnf();
let variants = match &*union_borrow {
- ValueF::UnionType(kts) => kts,
+ ValueKind::UnionType(kts) => kts,
_ => return mkerr(Merge2ArgMustBeUnion(union.clone())),
};
@@ -703,7 +704,7 @@ fn type_last_layer(
Some(Some(variant_type)) => {
let handler_type_borrow = handler_type.as_whnf();
let (x, tx, tb) = match &*handler_type_borrow {
- ValueF::Pi(x, tx, tb) => (x, tx, tb),
+ ValueKind::Pi(x, tx, tb) => (x, tx, tb),
_ => {
return mkerr(NotAFunction(
handler_type.clone(),
@@ -765,7 +766,7 @@ fn type_last_layer(
let record_type = record.get_type()?;
let record_type_borrow = record_type.as_whnf();
let kts = match &*record_type_borrow {
- ValueF::RecordType(kts) => kts,
+ ValueKind::RecordType(kts) => kts,
_ => return mkerr(ProjectionMustBeRecord),
};
@@ -777,8 +778,8 @@ fn type_last_layer(
};
}
- RetTypeOnly(Value::from_valuef_and_type(
- ValueF::RecordType(new_kts),
+ RetTypeOnly(Value::from_kind_and_type(
+ ValueKind::RecordType(new_kts),
record_type.get_type()?,
))
}
@@ -786,8 +787,8 @@ fn type_last_layer(
};
Ok(match ret {
- RetTypeOnly(typ) => Value::from_valuef_and_type_and_span(
- ValueF::PartialExpr(e),
+ RetTypeOnly(typ) => Value::from_kind_and_type_and_span(
+ ValueKind::PartialExpr(e),
typ,
span,
),
@@ -806,5 +807,5 @@ pub(crate) fn typecheck_with(
expr: Expr<Normalized>,
ty: Expr<Normalized>,
) -> Result<Value, TypeError> {
- typecheck(expr.rewrap(ExprF::Annot(expr.clone(), ty)))
+ typecheck(expr.rewrap(ExprKind::Annot(expr.clone(), ty)))
}
diff --git a/dhall/src/semantics/to_expr.rs b/dhall/src/semantics/to_expr.rs
new file mode 100644
index 0000000..b21fb29
--- /dev/null
+++ b/dhall/src/semantics/to_expr.rs
@@ -0,0 +1,105 @@
+use crate::semantics::core::value::Value;
+use crate::semantics::core::value::ValueKind;
+use crate::semantics::phase::typecheck::rc;
+use crate::semantics::phase::NormalizedExpr;
+use crate::syntax;
+use crate::syntax::{Builtin, ExprKind};
+
+#[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(ExprKind::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(ExprKind::Builtin(*b)), |acc, v| {
+ rc(ExprKind::App(acc, v))
+ }),
+ ValueKind::Pi(x, t, e) => rc(ExprKind::Pi(
+ x.to_label_maybe_alpha(opts.alpha),
+ t.to_expr(opts),
+ e.to_expr(opts),
+ )),
+ ValueKind::Var(v) => rc(ExprKind::Var(v.to_var(opts.alpha))),
+ ValueKind::Const(c) => rc(ExprKind::Const(*c)),
+ ValueKind::BoolLit(b) => rc(ExprKind::BoolLit(*b)),
+ ValueKind::NaturalLit(n) => rc(ExprKind::NaturalLit(*n)),
+ ValueKind::IntegerLit(n) => rc(ExprKind::IntegerLit(*n)),
+ ValueKind::DoubleLit(n) => rc(ExprKind::DoubleLit(*n)),
+ ValueKind::EmptyOptionalLit(n) => rc(ExprKind::App(
+ rc(ExprKind::Builtin(Builtin::OptionalNone)),
+ n.to_expr(opts),
+ )),
+ ValueKind::NEOptionalLit(n) => rc(ExprKind::SomeLit(n.to_expr(opts))),
+ ValueKind::EmptyListLit(n) => {
+ rc(ExprKind::EmptyListLit(rc(ExprKind::App(
+ rc(ExprKind::Builtin(Builtin::List)),
+ n.to_expr(opts),
+ ))))
+ }
+ ValueKind::NEListLit(elts) => rc(ExprKind::NEListLit(
+ elts.iter().map(|n| n.to_expr(opts)).collect(),
+ )),
+ ValueKind::RecordLit(kvs) => rc(ExprKind::RecordLit(
+ kvs.iter()
+ .map(|(k, v)| (k.clone(), v.to_expr(opts)))
+ .collect(),
+ )),
+ ValueKind::RecordType(kts) => rc(ExprKind::RecordType(
+ kts.iter()
+ .map(|(k, v)| (k.clone(), v.to_expr(opts)))
+ .collect(),
+ )),
+ ValueKind::UnionType(kts) => rc(ExprKind::UnionType(
+ kts.iter()
+ .map(|(k, v)| (k.clone(), v.as_ref().map(|v| v.to_expr(opts))))
+ .collect(),
+ )),
+ ValueKind::UnionConstructor(l, kts) => rc(ExprKind::Field(
+ ValueKind::UnionType(kts.clone()).to_expr(opts),
+ l.clone(),
+ )),
+ ValueKind::UnionLit(l, v, kts) => rc(ExprKind::App(
+ ValueKind::UnionConstructor(l.clone(), kts.clone()).to_expr(opts),
+ v.to_expr(opts),
+ )),
+ ValueKind::TextLit(elts) => rc(ExprKind::TextLit(
+ elts.iter()
+ .map(|contents| contents.map_ref(|e| e.to_expr(opts)))
+ .collect(),
+ )),
+ ValueKind::Equivalence(x, y) => rc(ExprKind::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-27 14:49:59 +0000