summaryrefslogtreecommitdiff
path: root/dhall/src/semantics/core/value.rs
diff options
context:
space:
mode:
Diffstat (limited to 'dhall/src/semantics/core/value.rs')
-rw-r--r--dhall/src/semantics/core/value.rs497
1 files changed, 374 insertions, 123 deletions
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 {
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-08 15:06:22 +0000