From 30bbf22fbfaead80322888eba7b7acdf908c3f3e Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Tue, 17 Dec 2019 15:00:44 +0000 Subject: Rename ValueF to ValueKind --- dhall/src/semantics/core/context.rs | 4 +- dhall/src/semantics/core/mod.rs | 2 +- dhall/src/semantics/core/value.rs | 70 +++---- dhall/src/semantics/core/value_kind.rs | 333 +++++++++++++++++++++++++++++++++ dhall/src/semantics/core/valuef.rs | 323 -------------------------------- dhall/src/semantics/core/var.rs | 2 +- dhall/src/semantics/phase/mod.rs | 14 +- dhall/src/semantics/phase/normalize.rs | 216 ++++++++++----------- dhall/src/semantics/phase/typecheck.rs | 72 +++---- 9 files changed, 523 insertions(+), 513 deletions(-) create mode 100644 dhall/src/semantics/core/value_kind.rs delete mode 100644 dhall/src/semantics/core/valuef.rs (limited to 'dhall/src/semantics') diff --git a/dhall/src/semantics/core/context.rs b/dhall/src/semantics/core/context.rs index d150e56..8861378 100644 --- a/dhall/src/semantics/core/context.rs +++ b/dhall/src/semantics/core/context.rs @@ -2,7 +2,7 @@ use std::collections::HashMap; use std::rc::Rc; use crate::semantics::core::value::Value; -use crate::semantics::core::valuef::ValueF; +use crate::semantics::core::value_kind::ValueKind; use crate::semantics::core::var::{AlphaVar, Shift, Subst}; use crate::semantics::error::TypeError; use crate::syntax::{Label, V}; @@ -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..bf3d390 100644 --- a/dhall/src/semantics/core/mod.rs +++ b/dhall/src/semantics/core/mod.rs @@ -1,4 +1,4 @@ pub mod context; pub mod value; -pub mod valuef; +pub mod value_kind; pub mod var; diff --git a/dhall/src/semantics/core/value.rs b/dhall/src/semantics/core/value.rs index 6e6739f..7403742 100644 --- a/dhall/src/semantics/core/value.rs +++ b/dhall/src/semantics/core/value.rs @@ -2,7 +2,7 @@ use std::cell::{Ref, RefCell, RefMut}; use std::rc::Rc; use crate::semantics::core::context::TypecheckContext; -use crate::semantics::core::valuef::ValueF; +use crate::semantics::core::value_kind::ValueKind; use crate::semantics::core::var::{AlphaVar, Shift, Subst}; use crate::semantics::error::{TypeError, TypeMessage}; use crate::semantics::phase::normalize::{apply_any, normalize_whnf}; @@ -15,12 +15,12 @@ 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 + /// 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 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 + /// 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, } @@ -32,7 +32,7 @@ use Form::{Unevaled, NF, WHNF}; #[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, span: Span, @@ -57,8 +57,8 @@ impl ValueInternal { fn into_value(self) -> Value { Value(Rc::new(RefCell::new(self))) } - fn as_valuef(&self) -> &ValueF { - &self.value + fn as_kind(&self) -> &ValueKind { + &self.kind } fn normalize_whnf(&mut self) { @@ -67,21 +67,21 @@ impl ValueInternal { // Dummy value in case the other closure panics || ValueInternal { form: Unevaled, - value: ValueF::Const(Const::Type), + kind: ValueKind::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), + kind: normalize_whnf(vint.kind, &ty), ty: vint.ty, span: vint.span, }, // `value` is `Sort` (Unevaled, None) => ValueInternal { form: NF, - value: ValueF::Const(Const::Sort), + kind: ValueKind::Const(Const::Sort), ty: None, span: vint.span, }, @@ -97,7 +97,7 @@ impl ValueInternal { self.normalize_nf(); } WHNF => { - self.value.normalize_mut(); + self.kind.normalize_mut(); self.form = NF; } // Already in NF @@ -116,10 +116,10 @@ impl ValueInternal { } 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 +128,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 +160,7 @@ impl Value { pub(crate) fn as_const(&self) -> Option { match &*self.as_whnf() { - ValueF::Const(c) => Some(*c), + ValueKind::Const(c) => Some(*c), _ => None, } } @@ -174,30 +174,30 @@ impl Value { fn as_internal_mut(&self) -> RefMut { 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 aprticular it may just be an /// unevaled PartialExpr. You probably want to use `as_whnf`. - fn as_valuef(&self) -> Ref { - Ref::map(self.as_internal(), ValueInternal::as_valuef) + fn as_kind(&self) -> Ref { + 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 { + pub(crate) fn as_whnf(&self) -> Ref { 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) + self.as_kind().to_expr(opts) } - pub(crate) fn to_whnf_ignore_type(&self) -> ValueF { + 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 +234,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, ) @@ -275,7 +275,7 @@ impl Shift for ValueInternal { fn shift(&self, delta: isize, var: &AlphaVar) -> Option { 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(), }) @@ -284,10 +284,10 @@ impl Shift for ValueInternal { impl Subst 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,7 +303,7 @@ impl Subst 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(), } @@ -321,11 +321,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/value_kind.rs b/dhall/src/semantics/core/value_kind.rs new file mode 100644 index 0000000..36ba068 --- /dev/null +++ b/dhall/src/semantics/core/value_kind.rs @@ -0,0 +1,333 @@ +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 `ValueKind`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 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), + + 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), + RecordType(HashMap), + RecordLit(HashMap), + UnionType(HashMap>), + UnionConstructor(Label, HashMap>), + UnionLit(Label, Value, HashMap>), + // Invariant: in whnf, this must not contain interpolations that are themselves TextLits, and + // contiguous text values must be merged. + TextLit(Vec>), + Equivalence(Value, Value), + // Invariant: in whnf, this must not contain a value captured by one of the variants above. + PartialExpr(ExprF), +} + +impl ValueKind { + pub(crate) fn into_value_with_type(self, t: Value) -> Value { + Value::from_kind_and_type(self, t) + } + + pub(crate) fn to_expr(&self, opts: ToExprOptions) -> NormalizedExpr { + match self { + ValueKind::Lam(x, t, e) => rc(ExprF::Lam( + x.to_label_maybe_alpha(opts.alpha), + t.to_expr(opts), + e.to_expr(opts), + )), + ValueKind::AppliedBuiltin(b, args) => args + .iter() + .map(|v| v.to_expr(opts)) + .fold(rc(ExprF::Builtin(*b)), |acc, v| rc(ExprF::App(acc, v))), + ValueKind::Pi(x, t, e) => rc(ExprF::Pi( + x.to_label_maybe_alpha(opts.alpha), + t.to_expr(opts), + e.to_expr(opts), + )), + ValueKind::Var(v) => rc(ExprF::Var(v.to_var(opts.alpha))), + ValueKind::Const(c) => rc(ExprF::Const(*c)), + ValueKind::BoolLit(b) => rc(ExprF::BoolLit(*b)), + ValueKind::NaturalLit(n) => rc(ExprF::NaturalLit(*n)), + ValueKind::IntegerLit(n) => rc(ExprF::IntegerLit(*n)), + ValueKind::DoubleLit(n) => rc(ExprF::DoubleLit(*n)), + ValueKind::EmptyOptionalLit(n) => rc(ExprF::App( + rc(ExprF::Builtin(Builtin::OptionalNone)), + n.to_expr(opts), + )), + ValueKind::NEOptionalLit(n) => rc(ExprF::SomeLit(n.to_expr(opts))), + ValueKind::EmptyListLit(n) => rc(ExprF::EmptyListLit(rc( + ExprF::App(rc(ExprF::Builtin(Builtin::List)), n.to_expr(opts)), + ))), + ValueKind::NEListLit(elts) => rc(ExprF::NEListLit( + elts.iter().map(|n| n.to_expr(opts)).collect(), + )), + ValueKind::RecordLit(kvs) => rc(ExprF::RecordLit( + kvs.iter() + .map(|(k, v)| (k.clone(), v.to_expr(opts))) + .collect(), + )), + ValueKind::RecordType(kts) => rc(ExprF::RecordType( + kts.iter() + .map(|(k, v)| (k.clone(), v.to_expr(opts))) + .collect(), + )), + ValueKind::UnionType(kts) => rc(ExprF::UnionType( + kts.iter() + .map(|(k, v)| { + (k.clone(), v.as_ref().map(|v| v.to_expr(opts))) + }) + .collect(), + )), + ValueKind::UnionConstructor(l, kts) => rc(ExprF::Field( + ValueKind::UnionType(kts.clone()).to_expr(opts), + l.clone(), + )), + ValueKind::UnionLit(l, v, kts) => rc(ExprF::App( + ValueKind::UnionConstructor(l.clone(), kts.clone()) + .to_expr(opts), + v.to_expr(opts), + )), + ValueKind::TextLit(elts) => rc(ExprF::TextLit( + elts.iter() + .map(|contents| contents.map_ref(|e| e.to_expr(opts))) + .collect(), + )), + ValueKind::Equivalence(x, y) => rc(ExprF::BinOp( + syntax::BinOp::Equivalence, + x.to_expr(opts), + y.to_expr(opts), + )), + ValueKind::PartialExpr(e) => rc(e.map_ref(|v| v.to_expr(opts))), + } + } + + 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 ValueKind { + fn shift(&self, delta: isize, var: &AlphaVar) -> Option { + 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 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), + ), + } + } +} 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), - - 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), - RecordType(HashMap), - RecordLit(HashMap), - UnionType(HashMap>), - UnionConstructor(Label, HashMap>), - UnionLit(Label, Value, HashMap>), - // Invariant: in whnf, this must not contain interpolations that are themselves TextLits, and - // contiguous text values must be merged. - TextLit(Vec>), - Equivalence(Value, Value), - // Invariant: in whnf, this must not contain a value captured by one of the variants above. - PartialExpr(ExprF), -} - -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 { - 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 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..77473f6 100644 --- a/dhall/src/semantics/core/var.rs +++ b/dhall/src/semantics/core/var.rs @@ -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); diff --git a/dhall/src/semantics/phase/mod.rs b/dhall/src/semantics/phase/mod.rs index 752c257..f27088c 100644 --- a/dhall/src/semantics/phase/mod.rs +++ b/dhall/src/semantics/phase/mod.rs @@ -2,7 +2,7 @@ use std::fmt::Display; use std::path::Path; use crate::semantics::core::value::{ToExprOptions, Value}; -use crate::semantics::core::valuef::ValueF; +use crate::semantics::core::value_kind::ValueKind; use crate::semantics::core::var::{AlphaVar, Shift, Subst}; use crate::semantics::error::{EncodeError, Error, ImportError, TypeError}; use crate::syntax::binary; @@ -91,8 +91,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) @@ -148,8 +148,8 @@ impl Typed { pub fn make_record_type( kts: impl Iterator, ) -> 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 +158,8 @@ impl Typed { pub fn make_union_type( kts: impl Iterator)>, ) -> 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..157d1f3 100644 --- a/dhall/src/semantics/phase/normalize.rs +++ b/dhall/src/semantics/phase/normalize.rs @@ -1,7 +1,7 @@ use std::collections::HashMap; use crate::semantics::core::value::Value; -use crate::semantics::core::valuef::ValueF; +use crate::semantics::core::value_kind::ValueKind; use crate::semantics::core::var::{AlphaLabel, AlphaVar, Shift, Subst}; use crate::semantics::phase::Normalized; use crate::syntax; @@ -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(ExprF::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(ExprF::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, 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 = 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(ExprF::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,7 +479,7 @@ where // Small helper enum to avoid repetition enum Ret<'a> { - ValueF(ValueF), + ValueKind(ValueKind), Value(Value), ValueRef(&'a Value), Expr(ExprF), @@ -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(ExprF::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, _, _) => { @@ -612,8 +612,8 @@ fn apply_binop<'a>( pub(crate) fn normalize_one_layer( expr: ExprF, ty: &Value, -) -> ValueF { - use ValueF::{ +) -> ValueKind { + use ValueKind::{ AppliedBuiltin, BoolLit, DoubleLit, EmptyListLit, IntegerLit, NEListLit, NEOptionalLit, NaturalLit, RecordLit, TextLit, UnionConstructor, UnionLit, UnionType, @@ -639,17 +639,17 @@ pub(crate) fn normalize_one_layer( } 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::BoolLit(b) => Ret::ValueKind(BoolLit(b)), + ExprF::NaturalLit(n) => Ret::ValueKind(NaturalLit(n)), + ExprF::IntegerLit(n) => Ret::ValueKind(IntegerLit(n)), + ExprF::DoubleLit(n) => Ret::ValueKind(DoubleLit(n)), + ExprF::SomeLit(e) => Ret::ValueKind(NEOptionalLit(e)), ExprF::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); @@ -658,10 +658,10 @@ pub(crate) fn normalize_one_layer( } } ExprF::NEListLit(elts) => { - Ret::ValueF(NEListLit(elts.into_iter().collect())) + Ret::ValueKind(NEListLit(elts.into_iter().collect())) } ExprF::RecordLit(kvs) => { - Ret::ValueF(RecordLit(kvs.into_iter().collect())) + Ret::ValueKind(RecordLit(kvs.into_iter().collect())) } ExprF::TextLit(elts) => { use InterpolatedTextContents::Expr; @@ -670,7 +670,7 @@ pub(crate) fn normalize_one_layer( 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) => { @@ -701,12 +701,12 @@ pub(crate) fn normalize_one_layer( }, ExprF::Projection(_, ref ls) if ls.is_empty() => { - Ret::ValueF(RecordLit(HashMap::new())) + Ret::ValueKind(RecordLit(HashMap::new())) } ExprF::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())) @@ -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); @@ -773,20 +773,20 @@ pub(crate) fn normalize_one_layer( }; 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/typecheck.rs b/dhall/src/semantics/phase/typecheck.rs index 59380a3..96a0b4b 100644 --- a/dhall/src/semantics/phase/typecheck.rs +++ b/dhall/src/semantics/phase/typecheck.rs @@ -3,7 +3,7 @@ use std::collections::HashMap; use crate::semantics::core::context::TypecheckContext; use crate::semantics::core::value::Value; -use crate::semantics::core::valuef::ValueF; +use crate::semantics::core::value_kind::ValueKind; use crate::semantics::core::var::{Shift, Subst}; use crate::semantics::error::{TypeError, TypeMessage}; use crate::semantics::phase::normalize::merge_maps; @@ -39,8 +39,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 +71,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 +116,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,13 +131,13 @@ 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(), } @@ -290,8 +290,8 @@ fn type_of_builtin(b: Builtin) -> Expr { 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(), ) } @@ -313,8 +313,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)?, ) } @@ -389,7 +389,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 +406,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 +415,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 +435,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 +482,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 +492,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 +553,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())), }; @@ -589,7 +589,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 +598,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())) } @@ -626,7 +626,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 +648,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 +684,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 +703,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 +765,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 +777,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 +786,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, ), -- cgit v1.2.3 From fd665388b6f1fd80ded9010640ac65cfebca7bc6 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Tue, 17 Dec 2019 16:00:51 +0000 Subject: Move out conversion from value back to ast to its own file --- dhall/src/semantics/core/value.rs | 25 +++----- dhall/src/semantics/core/value_kind.rs | 82 +++----------------------- dhall/src/semantics/mod.rs | 1 + dhall/src/semantics/phase/mod.rs | 7 ++- dhall/src/semantics/to_expr.rs | 101 +++++++++++++++++++++++++++++++++ 5 files changed, 125 insertions(+), 91 deletions(-) create mode 100644 dhall/src/semantics/to_expr.rs (limited to 'dhall/src/semantics') diff --git a/dhall/src/semantics/core/value.rs b/dhall/src/semantics/core/value.rs index 7403742..ad0861b 100644 --- a/dhall/src/semantics/core/value.rs +++ b/dhall/src/semantics/core/value.rs @@ -8,6 +8,7 @@ use crate::semantics::error::{TypeError, TypeMessage}; use crate::semantics::phase::normalize::{apply_any, normalize_whnf}; use crate::semantics::phase::typecheck::{builtin_to_value, const_to_value}; use crate::semantics::phase::{NormalizedExpr, Typed}; +use crate::semantics::to_expr; use crate::syntax::{Builtin, Const, Span}; #[derive(Debug, Clone, Copy)] @@ -44,15 +45,6 @@ struct ValueInternal { #[derive(Clone)] pub(crate) struct Value(Rc>); -#[derive(Copy, Clone)] -/// Controls conversion from `Value` to `Expr` -pub(crate) struct ToExprOptions { - /// Whether to convert all variables to `_` - pub(crate) alpha: bool, - /// Whether to normalize before converting - pub(crate) normalize: bool, -} - impl ValueInternal { fn into_value(self) -> Value { Value(Rc::new(RefCell::new(self))) @@ -174,9 +166,9 @@ impl Value { fn as_internal_mut(&self) -> RefMut { self.0.borrow_mut() } - /// WARNING: The returned ValueKind may be entirely unnormalized, in aprticular it may just be an + /// WARNING: The returned ValueKind may be entirely unnormalized, in particular it may just be an /// unevaled PartialExpr. You probably want to use `as_whnf`. - fn as_kind(&self) -> Ref { + pub(crate) fn as_kind(&self) -> Ref { Ref::map(self.as_internal(), ValueInternal::as_kind) } /// This is what you want if you want to pattern-match on the value. @@ -187,11 +179,12 @@ impl Value { self.as_kind() } - pub(crate) fn to_expr(&self, opts: ToExprOptions) -> NormalizedExpr { - if opts.normalize { - self.normalize_whnf(); - } - self.as_kind().to_expr(opts) + /// Converts a value back to the corresponding AST expression. + pub(crate) fn to_expr( + &self, + opts: to_expr::ToExprOptions, + ) -> NormalizedExpr { + to_expr::value_to_expr(self, opts) } pub(crate) fn to_whnf_ignore_type(&self) -> ValueKind { self.as_whnf().clone() diff --git a/dhall/src/semantics/core/value_kind.rs b/dhall/src/semantics/core/value_kind.rs index 36ba068..47df39d 100644 --- a/dhall/src/semantics/core/value_kind.rs +++ b/dhall/src/semantics/core/value_kind.rs @@ -1,10 +1,9 @@ use std::collections::HashMap; -use crate::semantics::core::value::{ToExprOptions, Value}; +use crate::semantics::core::value::Value; use crate::semantics::core::var::{AlphaLabel, AlphaVar, Shift, Subst}; -use crate::semantics::phase::typecheck::rc; use crate::semantics::phase::{Normalized, NormalizedExpr}; -use crate::syntax; +use crate::semantics::to_expr; use crate::syntax::{ Builtin, Const, ExprF, Integer, InterpolatedTextContents, Label, NaiveDouble, Natural, @@ -52,77 +51,12 @@ impl ValueKind { Value::from_kind_and_type(self, t) } - pub(crate) fn to_expr(&self, opts: ToExprOptions) -> NormalizedExpr { - match self { - ValueKind::Lam(x, t, e) => rc(ExprF::Lam( - x.to_label_maybe_alpha(opts.alpha), - t.to_expr(opts), - e.to_expr(opts), - )), - ValueKind::AppliedBuiltin(b, args) => args - .iter() - .map(|v| v.to_expr(opts)) - .fold(rc(ExprF::Builtin(*b)), |acc, v| rc(ExprF::App(acc, v))), - ValueKind::Pi(x, t, e) => rc(ExprF::Pi( - x.to_label_maybe_alpha(opts.alpha), - t.to_expr(opts), - e.to_expr(opts), - )), - ValueKind::Var(v) => rc(ExprF::Var(v.to_var(opts.alpha))), - ValueKind::Const(c) => rc(ExprF::Const(*c)), - ValueKind::BoolLit(b) => rc(ExprF::BoolLit(*b)), - ValueKind::NaturalLit(n) => rc(ExprF::NaturalLit(*n)), - ValueKind::IntegerLit(n) => rc(ExprF::IntegerLit(*n)), - ValueKind::DoubleLit(n) => rc(ExprF::DoubleLit(*n)), - ValueKind::EmptyOptionalLit(n) => rc(ExprF::App( - rc(ExprF::Builtin(Builtin::OptionalNone)), - n.to_expr(opts), - )), - ValueKind::NEOptionalLit(n) => rc(ExprF::SomeLit(n.to_expr(opts))), - ValueKind::EmptyListLit(n) => rc(ExprF::EmptyListLit(rc( - ExprF::App(rc(ExprF::Builtin(Builtin::List)), n.to_expr(opts)), - ))), - ValueKind::NEListLit(elts) => rc(ExprF::NEListLit( - elts.iter().map(|n| n.to_expr(opts)).collect(), - )), - ValueKind::RecordLit(kvs) => rc(ExprF::RecordLit( - kvs.iter() - .map(|(k, v)| (k.clone(), v.to_expr(opts))) - .collect(), - )), - ValueKind::RecordType(kts) => rc(ExprF::RecordType( - kts.iter() - .map(|(k, v)| (k.clone(), v.to_expr(opts))) - .collect(), - )), - ValueKind::UnionType(kts) => rc(ExprF::UnionType( - kts.iter() - .map(|(k, v)| { - (k.clone(), v.as_ref().map(|v| v.to_expr(opts))) - }) - .collect(), - )), - ValueKind::UnionConstructor(l, kts) => rc(ExprF::Field( - ValueKind::UnionType(kts.clone()).to_expr(opts), - l.clone(), - )), - ValueKind::UnionLit(l, v, kts) => rc(ExprF::App( - ValueKind::UnionConstructor(l.clone(), kts.clone()) - .to_expr(opts), - v.to_expr(opts), - )), - ValueKind::TextLit(elts) => rc(ExprF::TextLit( - elts.iter() - .map(|contents| contents.map_ref(|e| e.to_expr(opts))) - .collect(), - )), - ValueKind::Equivalence(x, y) => rc(ExprF::BinOp( - syntax::BinOp::Equivalence, - x.to_expr(opts), - y.to_expr(opts), - )), - ValueKind::PartialExpr(e) => rc(e.map_ref(|v| v.to_expr(opts))), - } + /// Converts a value back to the corresponding AST expression. + pub(crate) fn to_expr( + &self, + opts: to_expr::ToExprOptions, + ) -> NormalizedExpr { + to_expr::kind_to_expr(self, opts) } pub(crate) fn normalize_mut(&mut self) { diff --git a/dhall/src/semantics/mod.rs b/dhall/src/semantics/mod.rs index 9d2e462..6438408 100644 --- a/dhall/src/semantics/mod.rs +++ b/dhall/src/semantics/mod.rs @@ -1,3 +1,4 @@ pub mod core; pub mod error; pub mod phase; +pub mod to_expr; diff --git a/dhall/src/semantics/phase/mod.rs b/dhall/src/semantics/phase/mod.rs index f27088c..6229d15 100644 --- a/dhall/src/semantics/phase/mod.rs +++ b/dhall/src/semantics/phase/mod.rs @@ -1,10 +1,11 @@ use std::fmt::Display; use std::path::Path; -use crate::semantics::core::value::{ToExprOptions, Value}; +use crate::semantics::core::value::Value; use crate::semantics::core::value_kind::ValueKind; use crate::semantics::core::var::{AlphaVar, Shift, Subst}; use crate::semantics::error::{EncodeError, Error, ImportError, TypeError}; +use crate::semantics::to_expr::ToExprOptions; use crate::syntax::binary; use crate::syntax::{Builtin, Const, Expr}; use resolve::ImportRoot; @@ -101,18 +102,22 @@ impl Typed { Typed::from_const(Const::Type) } + /// Converts a value back to the corresponding AST expression. pub(crate) fn to_expr(&self) -> NormalizedExpr { self.0.to_expr(ToExprOptions { alpha: false, normalize: false, }) } + /// Converts a value back to the corresponding AST expression, normalizing in the process. pub fn normalize_to_expr(&self) -> NormalizedExpr { self.0.to_expr(ToExprOptions { alpha: false, normalize: true, }) } + /// Converts a value back to the corresponding AST expression, (akpha,beta)-normalizing in the + /// process. pub(crate) fn normalize_to_expr_alpha(&self) -> NormalizedExpr { self.0.to_expr(ToExprOptions { alpha: true, diff --git a/dhall/src/semantics/to_expr.rs b/dhall/src/semantics/to_expr.rs new file mode 100644 index 0000000..74bd2fe --- /dev/null +++ b/dhall/src/semantics/to_expr.rs @@ -0,0 +1,101 @@ +use crate::semantics::core::value::Value; +use crate::semantics::core::value_kind::ValueKind; +use crate::semantics::phase::typecheck::rc; +use crate::semantics::phase::NormalizedExpr; +use crate::syntax; +use crate::syntax::{Builtin, ExprF}; + +#[derive(Copy, Clone)] +/// Controls conversion from `Value` to `Expr` +pub(crate) struct ToExprOptions { + /// Whether to convert all variables to `_` + pub(crate) alpha: bool, + /// Whether to normalize before converting + pub(crate) normalize: bool, +} + +/// Converts a value back to the corresponding AST expression. +pub(crate) fn value_to_expr( + val: &Value, + opts: ToExprOptions, +) -> NormalizedExpr { + if opts.normalize { + val.normalize_whnf(); + } + val.as_kind().to_expr(opts) +} + +/// Converts a value back to the corresponding AST expression. +pub(crate) fn kind_to_expr( + kind: &ValueKind, + opts: ToExprOptions, +) -> NormalizedExpr { + match kind { + ValueKind::Lam(x, t, e) => rc(ExprF::Lam( + x.to_label_maybe_alpha(opts.alpha), + t.to_expr(opts), + e.to_expr(opts), + )), + ValueKind::AppliedBuiltin(b, args) => args + .iter() + .map(|v| v.to_expr(opts)) + .fold(rc(ExprF::Builtin(*b)), |acc, v| rc(ExprF::App(acc, v))), + ValueKind::Pi(x, t, e) => rc(ExprF::Pi( + x.to_label_maybe_alpha(opts.alpha), + t.to_expr(opts), + e.to_expr(opts), + )), + ValueKind::Var(v) => rc(ExprF::Var(v.to_var(opts.alpha))), + ValueKind::Const(c) => rc(ExprF::Const(*c)), + ValueKind::BoolLit(b) => rc(ExprF::BoolLit(*b)), + ValueKind::NaturalLit(n) => rc(ExprF::NaturalLit(*n)), + ValueKind::IntegerLit(n) => rc(ExprF::IntegerLit(*n)), + ValueKind::DoubleLit(n) => rc(ExprF::DoubleLit(*n)), + ValueKind::EmptyOptionalLit(n) => rc(ExprF::App( + rc(ExprF::Builtin(Builtin::OptionalNone)), + n.to_expr(opts), + )), + ValueKind::NEOptionalLit(n) => rc(ExprF::SomeLit(n.to_expr(opts))), + ValueKind::EmptyListLit(n) => rc(ExprF::EmptyListLit(rc(ExprF::App( + rc(ExprF::Builtin(Builtin::List)), + n.to_expr(opts), + )))), + ValueKind::NEListLit(elts) => rc(ExprF::NEListLit( + elts.iter().map(|n| n.to_expr(opts)).collect(), + )), + ValueKind::RecordLit(kvs) => rc(ExprF::RecordLit( + kvs.iter() + .map(|(k, v)| (k.clone(), v.to_expr(opts))) + .collect(), + )), + ValueKind::RecordType(kts) => rc(ExprF::RecordType( + kts.iter() + .map(|(k, v)| (k.clone(), v.to_expr(opts))) + .collect(), + )), + ValueKind::UnionType(kts) => rc(ExprF::UnionType( + kts.iter() + .map(|(k, v)| (k.clone(), v.as_ref().map(|v| v.to_expr(opts)))) + .collect(), + )), + ValueKind::UnionConstructor(l, kts) => rc(ExprF::Field( + ValueKind::UnionType(kts.clone()).to_expr(opts), + l.clone(), + )), + ValueKind::UnionLit(l, v, kts) => rc(ExprF::App( + ValueKind::UnionConstructor(l.clone(), kts.clone()).to_expr(opts), + v.to_expr(opts), + )), + ValueKind::TextLit(elts) => rc(ExprF::TextLit( + elts.iter() + .map(|contents| contents.map_ref(|e| e.to_expr(opts))) + .collect(), + )), + ValueKind::Equivalence(x, y) => rc(ExprF::BinOp( + syntax::BinOp::Equivalence, + x.to_expr(opts), + y.to_expr(opts), + )), + ValueKind::PartialExpr(e) => rc(e.map_ref(|v| v.to_expr(opts))), + } +} -- cgit v1.2.3 From 78d066a44c5598794602effa4c10a09f80ed1e72 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Fri, 20 Dec 2019 17:57:49 +0000 Subject: Move error module to root of crate --- dhall/src/semantics/core/context.rs | 2 +- dhall/src/semantics/core/value.rs | 2 +- dhall/src/semantics/error/mod.rs | 178 --------------------------------- dhall/src/semantics/mod.rs | 1 - dhall/src/semantics/phase/mod.rs | 2 +- dhall/src/semantics/phase/parse.rs | 2 +- dhall/src/semantics/phase/resolve.rs | 2 +- dhall/src/semantics/phase/typecheck.rs | 2 +- 8 files changed, 6 insertions(+), 185 deletions(-) delete mode 100644 dhall/src/semantics/error/mod.rs (limited to 'dhall/src/semantics') diff --git a/dhall/src/semantics/core/context.rs b/dhall/src/semantics/core/context.rs index 8861378..9dfd22b 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::value_kind::ValueKind; use crate::semantics::core::var::{AlphaVar, Shift, Subst}; -use crate::semantics::error::TypeError; use crate::syntax::{Label, V}; #[derive(Debug, Clone)] diff --git a/dhall/src/semantics/core/value.rs b/dhall/src/semantics/core/value.rs index ad0861b..9511cc2 100644 --- a/dhall/src/semantics/core/value.rs +++ b/dhall/src/semantics/core/value.rs @@ -1,10 +1,10 @@ use std::cell::{Ref, RefCell, RefMut}; use std::rc::Rc; +use crate::error::{TypeError, TypeMessage}; use crate::semantics::core::context::TypecheckContext; use crate::semantics::core::value_kind::ValueKind; use crate::semantics::core::var::{AlphaVar, Shift, Subst}; -use crate::semantics::error::{TypeError, TypeMessage}; use crate::semantics::phase::normalize::{apply_any, normalize_whnf}; use crate::semantics::phase::typecheck::{builtin_to_value, const_to_value}; use crate::semantics::phase::{NormalizedExpr, Typed}; 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 = std::result::Result; - -#[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, Box), - UnexpectedImport(Import), - ImportCycle(ImportStack, Import), -} - -#[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 for Error { - fn from(err: IOError) -> Error { - Error::IO(err) - } -} -impl From for Error { - fn from(err: ParseError) -> Error { - Error::Parse(err) - } -} -impl From for Error { - fn from(err: DecodeError) -> Error { - Error::Decode(err) - } -} -impl From for Error { - fn from(err: EncodeError) -> Error { - Error::Encode(err) - } -} -impl From for Error { - fn from(err: ImportError) -> Error { - Error::Resolve(err) - } -} -impl From 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 6438408..1eeef86 100644 --- a/dhall/src/semantics/mod.rs +++ b/dhall/src/semantics/mod.rs @@ -1,4 +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 6229d15..9359c0b 100644 --- a/dhall/src/semantics/phase/mod.rs +++ b/dhall/src/semantics/phase/mod.rs @@ -1,10 +1,10 @@ use std::fmt::Display; use std::path::Path; +use crate::error::{EncodeError, Error, ImportError, TypeError}; use crate::semantics::core::value::Value; use crate::semantics::core::value_kind::ValueKind; use crate::semantics::core::var::{AlphaVar, Shift, Subst}; -use crate::semantics::error::{EncodeError, Error, ImportError, TypeError}; use crate::semantics::to_expr::ToExprOptions; use crate::syntax::binary; use crate::syntax::{Builtin, Const, Expr}; 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 96a0b4b..5041235 100644 --- a/dhall/src/semantics/phase/typecheck.rs +++ b/dhall/src/semantics/phase/typecheck.rs @@ -1,11 +1,11 @@ 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::value_kind::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; -- cgit v1.2.3 From e355984c3c83f8288eac36023c361db869643367 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Fri, 20 Dec 2019 18:12:10 +0000 Subject: s/ExprF/ExprKind/ --- dhall/src/semantics/core/value_kind.rs | 4 +- dhall/src/semantics/core/var.rs | 6 +-- dhall/src/semantics/phase/normalize.rs | 76 +++++++++++++++++----------------- dhall/src/semantics/phase/typecheck.rs | 45 ++++++++++---------- dhall/src/semantics/to_expr.rs | 54 +++++++++++++----------- 5 files changed, 95 insertions(+), 90 deletions(-) (limited to 'dhall/src/semantics') diff --git a/dhall/src/semantics/core/value_kind.rs b/dhall/src/semantics/core/value_kind.rs index 47df39d..35b2b23 100644 --- a/dhall/src/semantics/core/value_kind.rs +++ b/dhall/src/semantics/core/value_kind.rs @@ -5,7 +5,7 @@ use crate::semantics::core::var::{AlphaLabel, AlphaVar, Shift, Subst}; use crate::semantics::phase::{Normalized, NormalizedExpr}; use crate::semantics::to_expr; use crate::syntax::{ - Builtin, Const, ExprF, Integer, InterpolatedTextContents, Label, + Builtin, Const, ExprKind, Integer, InterpolatedTextContents, Label, NaiveDouble, Natural, }; @@ -43,7 +43,7 @@ pub(crate) enum ValueKind { TextLit(Vec>), Equivalence(Value, Value), // Invariant: in whnf, this must not contain a value captured by one of the variants above. - PartialExpr(ExprF), + PartialExpr(ExprKind), } impl ValueKind { diff --git a/dhall/src/semantics/core/var.rs b/dhall/src/semantics/core/var.rs index 77473f6..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. @@ -190,7 +190,7 @@ impl Shift for std::cell::RefCell { } } -impl Shift for ExprF { +impl Shift for ExprKind { fn shift(&self, delta: isize, var: &AlphaVar) -> Option { Some(self.traverse_ref_with_special_handling_of_binders( |v| Ok(v.shift(delta, var)?), @@ -262,7 +262,7 @@ impl> Subst for std::cell::RefCell { } } -impl, E: Clone> Subst for ExprF { +impl, E: Clone> Subst for ExprKind { 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/phase/normalize.rs b/dhall/src/semantics/phase/normalize.rs index 157d1f3..3e612aa 100644 --- a/dhall/src/semantics/phase/normalize.rs +++ b/dhall/src/semantics/phase/normalize.rs @@ -7,8 +7,8 @@ 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 @@ -46,7 +46,7 @@ macro_rules! make_closure { ValueKind::NEOptionalLit(v).into_value_with_type(opt_v_type) }}; (1 + $($rest:tt)*) => { - ValueKind::PartialExpr(ExprF::BinOp( + ValueKind::PartialExpr(ExprKind::BinOp( syntax::BinOp::NaturalPlus, make_closure!($($rest)*), Value::from_kind_and_type( @@ -61,7 +61,7 @@ macro_rules! make_closure { let head = make_closure!($($head)*); let tail = make_closure!($($tail)*); let list_type = tail.get_type_not_sort(); - ValueKind::PartialExpr(ExprF::BinOp( + ValueKind::PartialExpr(ExprKind::BinOp( syntax::BinOp::ListAppend, ValueKind::NEListLit(vec![head]) .into_value_with_type(list_type.clone()), @@ -404,7 +404,7 @@ pub(crate) fn apply_any(f: Value, a: Value, ty: &Value) -> ValueKind { } _ => { drop(f_borrow); - ValueKind::PartialExpr(ExprF::App(f, a)) + ValueKind::PartialExpr(ExprKind::App(f, a)) } } } @@ -482,7 +482,7 @@ enum Ret<'a> { ValueKind(ValueKind), Value(Value), ValueRef(&'a Value), - Expr(ExprF), + Expr(ExprKind), } fn apply_binop<'a>( @@ -590,7 +590,7 @@ fn apply_binop<'a>( }; let kvs = merge_maps::<_, _, _, !>(kvs1, kvs2, |k, v1, v2| { Ok(Value::from_kind_and_type( - ValueKind::PartialExpr(ExprF::BinOp( + ValueKind::PartialExpr(ExprKind::BinOp( RecursiveRecordMerge, v1.clone(), v2.clone(), @@ -610,7 +610,7 @@ fn apply_binop<'a>( } pub(crate) fn normalize_one_layer( - expr: ExprF, + expr: ExprKind, ty: &Value, ) -> ValueKind { use ValueKind::{ @@ -620,31 +620,31 @@ pub(crate) fn normalize_one_layer( }; 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::ValueKind(BoolLit(b)), - ExprF::NaturalLit(n) => Ret::ValueKind(NaturalLit(n)), - ExprF::IntegerLit(n) => Ret::ValueKind(IntegerLit(n)), - ExprF::DoubleLit(n) => Ret::ValueKind(DoubleLit(n)), - ExprF::SomeLit(e) => Ret::ValueKind(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 { @@ -657,13 +657,13 @@ pub(crate) fn normalize_one_layer( } } } - ExprF::NEListLit(elts) => { + ExprKind::NEListLit(elts) => { Ret::ValueKind(NEListLit(elts.into_iter().collect())) } - ExprF::RecordLit(kvs) => { + 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 @@ -673,7 +673,7 @@ pub(crate) fn normalize_one_layer( 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,15 +695,15 @@ 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() => { + 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::ValueKind(RecordLit( @@ -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) { @@ -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,7 +769,7 @@ pub(crate) fn normalize_one_layer( } } } - ExprF::ToMap(_, _) => unimplemented!("toMap"), + ExprKind::ToMap(_, _) => unimplemented!("toMap"), }; match ret { diff --git a/dhall/src/semantics/phase/typecheck.rs b/dhall/src/semantics/phase/typecheck.rs index 5041235..f83bb94 100644 --- a/dhall/src/semantics/phase/typecheck.rs +++ b/dhall/src/semantics/phase/typecheck.rs @@ -10,7 +10,8 @@ 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, RawExpr, + Span, }; fn tck_pi_type( @@ -149,24 +150,24 @@ pub fn rc(x: RawExpr) -> Expr { // 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)*)) @@ -304,7 +305,7 @@ fn type_with( ctx: &TypecheckContext, e: Expr, ) -> Result { - 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() { @@ -359,13 +360,13 @@ fn type_with( /// layer. fn type_last_layer( ctx: &TypecheckContext, - e: ExprF, + e: ExprKind, span: Span, ) -> Result { 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)); @@ -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()?, @@ -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(), @@ -806,5 +807,5 @@ pub(crate) fn typecheck_with( expr: Expr, ty: Expr, ) -> Result { - 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 index 74bd2fe..6099976 100644 --- a/dhall/src/semantics/to_expr.rs +++ b/dhall/src/semantics/to_expr.rs @@ -3,7 +3,7 @@ use crate::semantics::core::value_kind::ValueKind; use crate::semantics::phase::typecheck::rc; use crate::semantics::phase::NormalizedExpr; use crate::syntax; -use crate::syntax::{Builtin, ExprF}; +use crate::syntax::{Builtin, ExprKind}; #[derive(Copy, Clone)] /// Controls conversion from `Value` to `Expr` @@ -31,7 +31,7 @@ pub(crate) fn kind_to_expr( opts: ToExprOptions, ) -> NormalizedExpr { match kind { - ValueKind::Lam(x, t, e) => rc(ExprF::Lam( + ValueKind::Lam(x, t, e) => rc(ExprKind::Lam( x.to_label_maybe_alpha(opts.alpha), t.to_expr(opts), e.to_expr(opts), @@ -39,59 +39,63 @@ pub(crate) fn kind_to_expr( ValueKind::AppliedBuiltin(b, args) => args .iter() .map(|v| v.to_expr(opts)) - .fold(rc(ExprF::Builtin(*b)), |acc, v| rc(ExprF::App(acc, v))), - ValueKind::Pi(x, t, e) => rc(ExprF::Pi( + .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(ExprF::Var(v.to_var(opts.alpha))), - ValueKind::Const(c) => rc(ExprF::Const(*c)), - ValueKind::BoolLit(b) => rc(ExprF::BoolLit(*b)), - ValueKind::NaturalLit(n) => rc(ExprF::NaturalLit(*n)), - ValueKind::IntegerLit(n) => rc(ExprF::IntegerLit(*n)), - ValueKind::DoubleLit(n) => rc(ExprF::DoubleLit(*n)), - ValueKind::EmptyOptionalLit(n) => rc(ExprF::App( - rc(ExprF::Builtin(Builtin::OptionalNone)), + 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(ExprF::SomeLit(n.to_expr(opts))), - ValueKind::EmptyListLit(n) => rc(ExprF::EmptyListLit(rc(ExprF::App( - rc(ExprF::Builtin(Builtin::List)), - n.to_expr(opts), - )))), - ValueKind::NEListLit(elts) => rc(ExprF::NEListLit( + 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(ExprF::RecordLit( + ValueKind::RecordLit(kvs) => rc(ExprKind::RecordLit( kvs.iter() .map(|(k, v)| (k.clone(), v.to_expr(opts))) .collect(), )), - ValueKind::RecordType(kts) => rc(ExprF::RecordType( + ValueKind::RecordType(kts) => rc(ExprKind::RecordType( kts.iter() .map(|(k, v)| (k.clone(), v.to_expr(opts))) .collect(), )), - ValueKind::UnionType(kts) => rc(ExprF::UnionType( + 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(ExprF::Field( + ValueKind::UnionConstructor(l, kts) => rc(ExprKind::Field( ValueKind::UnionType(kts.clone()).to_expr(opts), l.clone(), )), - ValueKind::UnionLit(l, v, kts) => rc(ExprF::App( + 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(ExprF::TextLit( + ValueKind::TextLit(elts) => rc(ExprKind::TextLit( elts.iter() .map(|contents| contents.map_ref(|e| e.to_expr(opts))) .collect(), )), - ValueKind::Equivalence(x, y) => rc(ExprF::BinOp( + ValueKind::Equivalence(x, y) => rc(ExprKind::BinOp( syntax::BinOp::Equivalence, x.to_expr(opts), y.to_expr(opts), -- cgit v1.2.3 From 980e50f33a88559edcf8b12cdec91fd9bee84ca9 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Fri, 20 Dec 2019 19:01:07 +0000 Subject: s/RawExpr/UnspannedExpr/ --- dhall/src/semantics/phase/typecheck.rs | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'dhall/src/semantics') diff --git a/dhall/src/semantics/phase/typecheck.rs b/dhall/src/semantics/phase/typecheck.rs index f83bb94..cf928d8 100644 --- a/dhall/src/semantics/phase/typecheck.rs +++ b/dhall/src/semantics/phase/typecheck.rs @@ -10,8 +10,8 @@ use crate::semantics::phase::normalize::merge_maps; use crate::semantics::phase::Normalized; use crate::syntax; use crate::syntax::{ - Builtin, Const, Expr, ExprKind, InterpolatedTextContents, Label, RawExpr, - Span, + Builtin, Const, Expr, ExprKind, InterpolatedTextContents, Label, Span, + UnspannedExpr, }; fn tck_pi_type( @@ -144,7 +144,7 @@ pub(crate) fn const_to_value(c: Const) -> Value { } } -pub fn rc(x: RawExpr) -> Expr { +pub fn rc(x: UnspannedExpr) -> Expr { Expr::new(x, Span::Artificial) } -- cgit v1.2.3 From 5c15f643236c5e14c2e8797b9dc507cffc93c43a Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Fri, 20 Dec 2019 19:15:10 +0000 Subject: Fix some comments --- dhall/src/semantics/phase/mod.rs | 11 ++--------- 1 file changed, 2 insertions(+), 9 deletions(-) (limited to 'dhall/src/semantics') diff --git a/dhall/src/semantics/phase/mod.rs b/dhall/src/semantics/phase/mod.rs index 9359c0b..7c57c3f 100644 --- a/dhall/src/semantics/phase/mod.rs +++ b/dhall/src/semantics/phase/mod.rs @@ -77,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) @@ -109,14 +102,14 @@ impl Typed { normalize: false, }) } - /// Converts a value back to the corresponding AST expression, normalizing in the process. + /// 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, (akpha,beta)-normalizing in the + /// 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 { -- cgit v1.2.3 From bc51d829f8b725531159a190f0096061df30b2cb Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Fri, 20 Dec 2019 19:18:40 +0000 Subject: Reorder value.rs --- dhall/src/semantics/core/value.rs | 162 +++++++++++++++++++------------------- 1 file changed, 81 insertions(+), 81 deletions(-) (limited to 'dhall/src/semantics') diff --git a/dhall/src/semantics/core/value.rs b/dhall/src/semantics/core/value.rs index 9511cc2..1e3b965 100644 --- a/dhall/src/semantics/core/value.rs +++ b/dhall/src/semantics/core/value.rs @@ -11,6 +11,25 @@ use crate::semantics::phase::{NormalizedExpr, Typed}; use crate::semantics::to_expr; use crate::syntax::{Builtin, Const, Span}; +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. +#[derive(Clone)] +pub(crate) struct Value(Rc>); + +/// 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, + kind: ValueKind, + /// This is None if and only if `value` is `Sort` (which doesn't have a type) + ty: Option, + span: Span, +} + #[derive(Debug, Clone, Copy)] pub(crate) enum Form { /// No constraints; expression may not be normalized at all. @@ -25,87 +44,6 @@ pub(crate) enum Form { /// if we have the first constructor of the NF at all levels, we actually have the NF. NF, } -use Form::{Unevaled, NF, WHNF}; - -/// 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, - kind: ValueKind, - /// This is None if and only if `value` is `Sort` (which doesn't have a type) - ty: Option, - 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>); - -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 Value { fn new(kind: ValueKind, form: Form, ty: Value, span: Span) -> Value { @@ -258,6 +196,68 @@ 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 Shift for Value { fn shift(&self, delta: isize, var: &AlphaVar) -> Option { Some(Value(self.0.shift(delta, var)?)) -- cgit v1.2.3 From 64cca1837cc97b7679c4e2ffd54a22ad50f05cfd Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Fri, 20 Dec 2019 19:26:08 +0000 Subject: Move ValueKind into value.rs --- dhall/src/semantics/core/context.rs | 2 +- dhall/src/semantics/core/mod.rs | 1 - dhall/src/semantics/core/value.rs | 270 ++++++++++++++++++++++++++++++++- dhall/src/semantics/core/value_kind.rs | 267 -------------------------------- dhall/src/semantics/phase/mod.rs | 2 +- dhall/src/semantics/phase/normalize.rs | 2 +- dhall/src/semantics/phase/typecheck.rs | 2 +- dhall/src/semantics/to_expr.rs | 2 +- 8 files changed, 269 insertions(+), 279 deletions(-) delete mode 100644 dhall/src/semantics/core/value_kind.rs (limited to 'dhall/src/semantics') diff --git a/dhall/src/semantics/core/context.rs b/dhall/src/semantics/core/context.rs index 9dfd22b..f755f72 100644 --- a/dhall/src/semantics/core/context.rs +++ b/dhall/src/semantics/core/context.rs @@ -3,7 +3,7 @@ use std::rc::Rc; use crate::error::TypeError; use crate::semantics::core::value::Value; -use crate::semantics::core::value_kind::ValueKind; +use crate::semantics::core::value::ValueKind; use crate::semantics::core::var::{AlphaVar, Shift, Subst}; use crate::syntax::{Label, V}; diff --git a/dhall/src/semantics/core/mod.rs b/dhall/src/semantics/core/mod.rs index bf3d390..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 value_kind; pub mod var; diff --git a/dhall/src/semantics/core/value.rs b/dhall/src/semantics/core/value.rs index 1e3b965..ca7c4bc 100644 --- a/dhall/src/semantics/core/value.rs +++ b/dhall/src/semantics/core/value.rs @@ -1,21 +1,27 @@ 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::value_kind::ValueKind; -use crate::semantics::core::var::{AlphaVar, Shift, Subst}; +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::semantics::phase::{Normalized, NormalizedExpr, Typed}; use crate::semantics::to_expr; -use crate::syntax::{Builtin, Const, Span}; +use crate::syntax::{ + Builtin, Const, ExprKind, Integer, InterpolatedTextContents, Label, + NaiveDouble, Natural, Span, +}; 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. +/// 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>); @@ -45,6 +51,38 @@ pub(crate) enum Form { 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), + + 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), + RecordType(HashMap), + RecordLit(HashMap), + UnionType(HashMap>), + UnionConstructor(Label, HashMap>), + UnionLit(Label, Value, HashMap>), + // Invariant: in whnf, this must not contain interpolations that are themselves TextLits, and + // contiguous text values must be merged. + TextLit(Vec>), + Equivalence(Value, Value), + // Invariant: in whnf, this must not contain a value captured by one of the variants above. + PartialExpr(ExprKind), +} + impl Value { fn new(kind: ValueKind, form: Form, ty: Value, span: Span) -> Value { ValueInternal { @@ -258,6 +296,94 @@ impl ValueInternal { } } +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 { Some(Value(self.0.shift(delta, var)?)) @@ -275,6 +401,71 @@ impl Shift for ValueInternal { } } +impl Shift for ValueKind { + fn shift(&self, delta: isize, var: &AlphaVar) -> Option { + 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 for Value { fn subst_shift(&self, var: &AlphaVar, val: &Value) -> Self { match &*self.as_kind() { @@ -303,6 +494,73 @@ impl Subst for ValueInternal { } } +impl Subst 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 { diff --git a/dhall/src/semantics/core/value_kind.rs b/dhall/src/semantics/core/value_kind.rs deleted file mode 100644 index 35b2b23..0000000 --- a/dhall/src/semantics/core/value_kind.rs +++ /dev/null @@ -1,267 +0,0 @@ -use std::collections::HashMap; - -use crate::semantics::core::value::Value; -use crate::semantics::core::var::{AlphaLabel, AlphaVar, Shift, Subst}; -use crate::semantics::phase::{Normalized, NormalizedExpr}; -use crate::semantics::to_expr; -use crate::syntax::{ - Builtin, Const, ExprKind, 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 `ValueKind`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 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), - - 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), - RecordType(HashMap), - RecordLit(HashMap), - UnionType(HashMap>), - UnionConstructor(Label, HashMap>), - UnionLit(Label, Value, HashMap>), - // Invariant: in whnf, this must not contain interpolations that are themselves TextLits, and - // contiguous text values must be merged. - TextLit(Vec>), - Equivalence(Value, Value), - // Invariant: in whnf, this must not contain a value captured by one of the variants above. - PartialExpr(ExprKind), -} - -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 ValueKind { - fn shift(&self, delta: isize, var: &AlphaVar) -> Option { - 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 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), - ), - } - } -} diff --git a/dhall/src/semantics/phase/mod.rs b/dhall/src/semantics/phase/mod.rs index 7c57c3f..b22120d 100644 --- a/dhall/src/semantics/phase/mod.rs +++ b/dhall/src/semantics/phase/mod.rs @@ -3,7 +3,7 @@ use std::path::Path; use crate::error::{EncodeError, Error, ImportError, TypeError}; use crate::semantics::core::value::Value; -use crate::semantics::core::value_kind::ValueKind; +use crate::semantics::core::value::ValueKind; use crate::semantics::core::var::{AlphaVar, Shift, Subst}; use crate::semantics::to_expr::ToExprOptions; use crate::syntax::binary; diff --git a/dhall/src/semantics/phase/normalize.rs b/dhall/src/semantics/phase/normalize.rs index 3e612aa..d81a910 100644 --- a/dhall/src/semantics/phase/normalize.rs +++ b/dhall/src/semantics/phase/normalize.rs @@ -1,7 +1,7 @@ use std::collections::HashMap; use crate::semantics::core::value::Value; -use crate::semantics::core::value_kind::ValueKind; +use crate::semantics::core::value::ValueKind; use crate::semantics::core::var::{AlphaLabel, AlphaVar, Shift, Subst}; use crate::semantics::phase::Normalized; use crate::syntax; diff --git a/dhall/src/semantics/phase/typecheck.rs b/dhall/src/semantics/phase/typecheck.rs index cf928d8..c439f74 100644 --- a/dhall/src/semantics/phase/typecheck.rs +++ b/dhall/src/semantics/phase/typecheck.rs @@ -4,7 +4,7 @@ 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::value_kind::ValueKind; +use crate::semantics::core::value::ValueKind; use crate::semantics::core::var::{Shift, Subst}; use crate::semantics::phase::normalize::merge_maps; use crate::semantics::phase::Normalized; diff --git a/dhall/src/semantics/to_expr.rs b/dhall/src/semantics/to_expr.rs index 6099976..b21fb29 100644 --- a/dhall/src/semantics/to_expr.rs +++ b/dhall/src/semantics/to_expr.rs @@ -1,5 +1,5 @@ use crate::semantics::core::value::Value; -use crate::semantics::core::value_kind::ValueKind; +use crate::semantics::core::value::ValueKind; use crate::semantics::phase::typecheck::rc; use crate::semantics::phase::NormalizedExpr; use crate::syntax; -- cgit v1.2.3