diff options
Diffstat (limited to 'dhall')
29 files changed, 1003 insertions, 1048 deletions
diff --git a/dhall/src/semantics/error/mod.rs b/dhall/src/error/mod.rs index 1288c12..1288c12 100644 --- a/dhall/src/semantics/error/mod.rs +++ b/dhall/src/error/mod.rs diff --git a/dhall/src/lib.rs b/dhall/src/lib.rs index 0991375..12660b4 100644 --- a/dhall/src/lib.rs +++ b/dhall/src/lib.rs @@ -12,5 +12,6 @@ mod tests; +pub mod error; pub mod semantics; pub mod syntax; diff --git a/dhall/src/semantics/core/context.rs b/dhall/src/semantics/core/context.rs index d150e56..f755f72 100644 --- a/dhall/src/semantics/core/context.rs +++ b/dhall/src/semantics/core/context.rs @@ -1,10 +1,10 @@ use std::collections::HashMap; use std::rc::Rc; +use crate::error::TypeError; use crate::semantics::core::value::Value; -use crate::semantics::core::valuef::ValueF; +use crate::semantics::core::value::ValueKind; use crate::semantics::core::var::{AlphaVar, Shift, Subst}; -use crate::semantics::error::TypeError; use crate::syntax::{Label, V}; #[derive(Debug, Clone)] @@ -39,7 +39,7 @@ impl TypecheckContext { let i = i.under_multiple_binders(&shift_map); return Some(match i { CtxItem::Kept(newvar, t) => { - Value::from_valuef_and_type(ValueF::Var(newvar), t) + Value::from_kind_and_type(ValueKind::Var(newvar), t) } CtxItem::Replaced(v) => v, }); diff --git a/dhall/src/semantics/core/mod.rs b/dhall/src/semantics/core/mod.rs index 08213f7..90d74ea 100644 --- a/dhall/src/semantics/core/mod.rs +++ b/dhall/src/semantics/core/mod.rs @@ -1,4 +1,3 @@ pub mod context; pub mod value; -pub mod valuef; pub mod var; diff --git a/dhall/src/semantics/core/value.rs b/dhall/src/semantics/core/value.rs index 6e6739f..ca7c4bc 100644 --- a/dhall/src/semantics/core/value.rs +++ b/dhall/src/semantics/core/value.rs @@ -1,125 +1,93 @@ use std::cell::{Ref, RefCell, RefMut}; +use std::collections::HashMap; use std::rc::Rc; +use crate::error::{TypeError, TypeMessage}; use crate::semantics::core::context::TypecheckContext; -use crate::semantics::core::valuef::ValueF; -use crate::semantics::core::var::{AlphaVar, Shift, Subst}; -use crate::semantics::error::{TypeError, TypeMessage}; +use crate::semantics::core::var::{AlphaLabel, AlphaVar, Shift, Subst}; use crate::semantics::phase::normalize::{apply_any, normalize_whnf}; use crate::semantics::phase::typecheck::{builtin_to_value, const_to_value}; -use crate::semantics::phase::{NormalizedExpr, Typed}; -use crate::syntax::{Builtin, Const, Span}; +use crate::semantics::phase::{Normalized, NormalizedExpr, Typed}; +use crate::semantics::to_expr; +use crate::syntax::{ + Builtin, Const, ExprKind, Integer, InterpolatedTextContents, Label, + NaiveDouble, Natural, Span, +}; -#[derive(Debug, Clone, Copy)] -pub(crate) enum Form { - /// No constraints; expression may not be normalized at all. - Unevaled, - /// Weak Head Normal Form, i.e. normalized up to the first constructor, but subexpressions may - /// not be normalized. This means that the first constructor of the contained ValueF is the first - /// constructor of the final Normal Form (NF). - WHNF, - /// Normal Form, i.e. completely normalized. - /// When all the Values in a ValueF are at least in WHNF, and recursively so, then the - /// ValueF is in NF. This is because WHNF ensures that we have the first constructor of the NF; so - /// if we have the first constructor of the NF at all levels, we actually have the NF. - NF, -} -use Form::{Unevaled, NF, WHNF}; +use self::Form::{Unevaled, NF, WHNF}; + +/// Stores a possibly unevaluated value. Gets (partially) normalized on-demand, sharing computation +/// automatically. Uses a RefCell to share computation. +/// Can optionally store a type from typechecking to preserve type information. +/// If you compare for equality two `Value`s in WHNF, then equality will be up to alpha-equivalence +/// (renaming of bound variables) and beta-equivalence (normalization). It will recursively +/// normalize as needed. +#[derive(Clone)] +pub(crate) struct Value(Rc<RefCell<ValueInternal>>); -/// Partially normalized value. /// Invariant: if `form` is `WHNF`, `value` must be in Weak Head Normal Form /// Invariant: if `form` is `NF`, `value` must be fully normalized #[derive(Debug)] struct ValueInternal { form: Form, - value: ValueF, + kind: ValueKind, /// This is None if and only if `value` is `Sort` (which doesn't have a type) ty: Option<Value>, span: Span, } -/// Stores a possibly unevaluated value. Gets (partially) normalized on-demand, -/// sharing computation automatically. Uses a RefCell to share computation. -/// Can optionally store a type from typechecking to preserve type information. -#[derive(Clone)] -pub(crate) struct Value(Rc<RefCell<ValueInternal>>); - -#[derive(Copy, Clone)] -/// Controls conversion from `Value` to `Expr` -pub(crate) struct ToExprOptions { - /// Whether to convert all variables to `_` - pub(crate) alpha: bool, - /// Whether to normalize before converting - pub(crate) normalize: bool, +#[derive(Debug, Clone, Copy)] +pub(crate) enum Form { + /// No constraints; expression may not be normalized at all. + Unevaled, + /// Weak Head Normal Form, i.e. normalized up to the first constructor, but subexpressions may + /// not be normalized. This means that the first constructor of the contained ValueKind is the first + /// constructor of the final Normal Form (NF). + WHNF, + /// Normal Form, i.e. completely normalized. + /// When all the Values in a ValueKind are at least in WHNF, and recursively so, then the + /// ValueKind is in NF. This is because WHNF ensures that we have the first constructor of the NF; so + /// if we have the first constructor of the NF at all levels, we actually have the NF. + NF, } -impl ValueInternal { - fn into_value(self) -> Value { - Value(Rc::new(RefCell::new(self))) - } - fn as_valuef(&self) -> &ValueF { - &self.value - } - - fn normalize_whnf(&mut self) { - take_mut::take_or_recover( - self, - // Dummy value in case the other closure panics - || ValueInternal { - form: Unevaled, - value: ValueF::Const(Const::Type), - ty: None, - span: Span::Artificial, - }, - |vint| match (&vint.form, &vint.ty) { - (Unevaled, Some(ty)) => ValueInternal { - form: WHNF, - value: normalize_whnf(vint.value, &ty), - ty: vint.ty, - span: vint.span, - }, - // `value` is `Sort` - (Unevaled, None) => ValueInternal { - form: NF, - value: ValueF::Const(Const::Sort), - ty: None, - span: vint.span, - }, - // Already in WHNF - (WHNF, _) | (NF, _) => vint, - }, - ) - } - fn normalize_nf(&mut self) { - match self.form { - Unevaled => { - self.normalize_whnf(); - self.normalize_nf(); - } - WHNF => { - self.value.normalize_mut(); - self.form = NF; - } - // Already in NF - NF => {} - } - } +#[derive(Debug, Clone, PartialEq, Eq)] +pub(crate) enum ValueKind { + /// Closures + Lam(AlphaLabel, Value, Value), + Pi(AlphaLabel, Value, Value), + // Invariant: in whnf, the evaluation must not be able to progress further. + AppliedBuiltin(Builtin, Vec<Value>), - fn get_type(&self) -> Result<&Value, TypeError> { - match &self.ty { - Some(t) => Ok(t), - None => { - Err(TypeError::new(&TypecheckContext::new(), TypeMessage::Sort)) - } - } - } + Var(AlphaVar), + Const(Const), + BoolLit(bool), + NaturalLit(Natural), + IntegerLit(Integer), + DoubleLit(NaiveDouble), + EmptyOptionalLit(Value), + NEOptionalLit(Value), + // EmptyListLit(t) means `[] : List t`, not `[] : t` + EmptyListLit(Value), + NEListLit(Vec<Value>), + RecordType(HashMap<Label, Value>), + RecordLit(HashMap<Label, Value>), + UnionType(HashMap<Label, Option<Value>>), + UnionConstructor(Label, HashMap<Label, Option<Value>>), + UnionLit(Label, Value, HashMap<Label, Option<Value>>), + // Invariant: in whnf, this must not contain interpolations that are themselves TextLits, and + // contiguous text values must be merged. + TextLit(Vec<InterpolatedTextContents<Value>>), + Equivalence(Value, Value), + // Invariant: in whnf, this must not contain a value captured by one of the variants above. + PartialExpr(ExprKind<Value, Normalized>), } impl Value { - fn new(value: ValueF, form: Form, ty: Value, span: Span) -> Value { + fn new(kind: ValueKind, form: Form, ty: Value, span: Span) -> Value { ValueInternal { form, - value, + kind, ty: Some(ty), span, } @@ -128,23 +96,23 @@ impl Value { pub(crate) fn const_sort() -> Value { ValueInternal { form: NF, - value: ValueF::Const(Const::Sort), + kind: ValueKind::Const(Const::Sort), ty: None, span: Span::Artificial, } .into_value() } - pub(crate) fn from_valuef_and_type(v: ValueF, t: Value) -> Value { + pub(crate) fn from_kind_and_type(v: ValueKind, t: Value) -> Value { Value::new(v, Unevaled, t, Span::Artificial) } - pub(crate) fn from_valuef_and_type_and_span( - v: ValueF, + pub(crate) fn from_kind_and_type_and_span( + v: ValueKind, t: Value, span: Span, ) -> Value { Value::new(v, Unevaled, t, span) } - pub(crate) fn from_valuef_and_type_whnf(v: ValueF, t: Value) -> Value { + pub(crate) fn from_kind_and_type_whnf(v: ValueKind, t: Value) -> Value { Value::new(v, WHNF, t, Span::Artificial) } pub(crate) fn from_const(c: Const) -> Self { @@ -160,7 +128,7 @@ impl Value { pub(crate) fn as_const(&self) -> Option<Const> { match &*self.as_whnf() { - ValueF::Const(c) => Some(*c), + ValueKind::Const(c) => Some(*c), _ => None, } } @@ -174,30 +142,31 @@ impl Value { fn as_internal_mut(&self) -> RefMut<ValueInternal> { self.0.borrow_mut() } - /// WARNING: The returned ValueF may be entirely unnormalized, in aprticular it may just be an + /// WARNING: The returned ValueKind may be entirely unnormalized, in particular it may just be an /// unevaled PartialExpr. You probably want to use `as_whnf`. - fn as_valuef(&self) -> Ref<ValueF> { - Ref::map(self.as_internal(), ValueInternal::as_valuef) + pub(crate) fn as_kind(&self) -> Ref<ValueKind> { + Ref::map(self.as_internal(), ValueInternal::as_kind) } /// This is what you want if you want to pattern-match on the value. /// WARNING: drop this ref before normalizing the same value or you will run into BorrowMut /// panics. - pub(crate) fn as_whnf(&self) -> Ref<ValueF> { + pub(crate) fn as_whnf(&self) -> Ref<ValueKind> { self.normalize_whnf(); - self.as_valuef() + self.as_kind() } - pub(crate) fn to_expr(&self, opts: ToExprOptions) -> NormalizedExpr { - if opts.normalize { - self.normalize_whnf(); - } - self.as_valuef().to_expr(opts) - } - pub(crate) fn to_whnf_ignore_type(&self) -> ValueF { + /// Converts a value back to the corresponding AST expression. + pub(crate) fn to_expr( + &self, + opts: to_expr::ToExprOptions, + ) -> NormalizedExpr { + to_expr::value_to_expr(self, opts) + } + pub(crate) fn to_whnf_ignore_type(&self) -> ValueKind { self.as_whnf().clone() } /// Before discarding type information, check that it matches the expected return type. - pub(crate) fn to_whnf_check_type(&self, ty: &Value) -> ValueF { + pub(crate) fn to_whnf_check_type(&self, ty: &Value) -> ValueKind { self.check_type(ty); self.to_whnf_ignore_type() } @@ -234,13 +203,13 @@ impl Value { pub(crate) fn app(&self, v: Value) -> Value { let body_t = match &*self.get_type_not_sort().as_whnf() { - ValueF::Pi(x, t, e) => { + ValueKind::Pi(x, t, e) => { v.check_type(t); e.subst_shift(&x.into(), &v) } _ => unreachable!("Internal type error"), }; - Value::from_valuef_and_type_whnf( + Value::from_kind_and_type_whnf( apply_any(self.clone(), v, &body_t), body_t, ) @@ -265,6 +234,156 @@ impl Value { } } +impl ValueInternal { + fn into_value(self) -> Value { + Value(Rc::new(RefCell::new(self))) + } + fn as_kind(&self) -> &ValueKind { + &self.kind + } + + fn normalize_whnf(&mut self) { + take_mut::take_or_recover( + self, + // Dummy value in case the other closure panics + || ValueInternal { + form: Unevaled, + kind: ValueKind::Const(Const::Type), + ty: None, + span: Span::Artificial, + }, + |vint| match (&vint.form, &vint.ty) { + (Unevaled, Some(ty)) => ValueInternal { + form: WHNF, + kind: normalize_whnf(vint.kind, &ty), + ty: vint.ty, + span: vint.span, + }, + // `value` is `Sort` + (Unevaled, None) => ValueInternal { + form: NF, + kind: ValueKind::Const(Const::Sort), + ty: None, + span: vint.span, + }, + // Already in WHNF + (WHNF, _) | (NF, _) => vint, + }, + ) + } + fn normalize_nf(&mut self) { + match self.form { + Unevaled => { + self.normalize_whnf(); + self.normalize_nf(); + } + WHNF => { + self.kind.normalize_mut(); + self.form = NF; + } + // Already in NF + NF => {} + } + } + + fn get_type(&self) -> Result<&Value, TypeError> { + match &self.ty { + Some(t) => Ok(t), + None => { + Err(TypeError::new(&TypecheckContext::new(), TypeMessage::Sort)) + } + } + } +} + +impl ValueKind { + pub(crate) fn into_value_with_type(self, t: Value) -> Value { + Value::from_kind_and_type(self, t) + } + + /// Converts a value back to the corresponding AST expression. + pub(crate) fn to_expr( + &self, + opts: to_expr::ToExprOptions, + ) -> NormalizedExpr { + to_expr::kind_to_expr(self, opts) + } + + pub(crate) fn normalize_mut(&mut self) { + match self { + ValueKind::Var(_) + | ValueKind::Const(_) + | ValueKind::BoolLit(_) + | ValueKind::NaturalLit(_) + | ValueKind::IntegerLit(_) + | ValueKind::DoubleLit(_) => {} + + ValueKind::EmptyOptionalLit(tth) | ValueKind::EmptyListLit(tth) => { + tth.normalize_mut(); + } + + ValueKind::NEOptionalLit(th) => { + th.normalize_mut(); + } + ValueKind::Lam(_, t, e) => { + t.normalize_mut(); + e.normalize_mut(); + } + ValueKind::Pi(_, t, e) => { + t.normalize_mut(); + e.normalize_mut(); + } + ValueKind::AppliedBuiltin(_, args) => { + for x in args.iter_mut() { + x.normalize_mut(); + } + } + ValueKind::NEListLit(elts) => { + for x in elts.iter_mut() { + x.normalize_mut(); + } + } + ValueKind::RecordLit(kvs) => { + for x in kvs.values_mut() { + x.normalize_mut(); + } + } + ValueKind::RecordType(kvs) => { + for x in kvs.values_mut() { + x.normalize_mut(); + } + } + ValueKind::UnionType(kts) | ValueKind::UnionConstructor(_, kts) => { + for x in kts.values_mut().flat_map(|opt| opt) { + x.normalize_mut(); + } + } + ValueKind::UnionLit(_, v, kts) => { + v.normalize_mut(); + for x in kts.values_mut().flat_map(|opt| opt) { + x.normalize_mut(); + } + } + ValueKind::TextLit(elts) => { + for x in elts.iter_mut() { + x.map_mut(Value::normalize_mut); + } + } + ValueKind::Equivalence(x, y) => { + x.normalize_mut(); + y.normalize_mut(); + } + ValueKind::PartialExpr(e) => { + e.map_mut(Value::normalize_mut); + } + } + } + + pub(crate) fn from_builtin(b: Builtin) -> ValueKind { + ValueKind::AppliedBuiltin(b, vec![]) + } +} + impl Shift for Value { fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> { Some(Value(self.0.shift(delta, var)?)) @@ -275,19 +394,84 @@ impl Shift for ValueInternal { fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> { Some(ValueInternal { form: self.form, - value: self.value.shift(delta, var)?, + kind: self.kind.shift(delta, var)?, ty: self.ty.shift(delta, var)?, span: self.span.clone(), }) } } +impl Shift for ValueKind { + fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> { + Some(match self { + ValueKind::Lam(x, t, e) => ValueKind::Lam( + x.clone(), + t.shift(delta, var)?, + e.shift(delta, &var.under_binder(x))?, + ), + ValueKind::AppliedBuiltin(b, args) => { + ValueKind::AppliedBuiltin(*b, args.shift(delta, var)?) + } + ValueKind::Pi(x, t, e) => ValueKind::Pi( + x.clone(), + t.shift(delta, var)?, + e.shift(delta, &var.under_binder(x))?, + ), + ValueKind::Var(v) => ValueKind::Var(v.shift(delta, var)?), + ValueKind::Const(c) => ValueKind::Const(*c), + ValueKind::BoolLit(b) => ValueKind::BoolLit(*b), + ValueKind::NaturalLit(n) => ValueKind::NaturalLit(*n), + ValueKind::IntegerLit(n) => ValueKind::IntegerLit(*n), + ValueKind::DoubleLit(n) => ValueKind::DoubleLit(*n), + ValueKind::EmptyOptionalLit(tth) => { + ValueKind::EmptyOptionalLit(tth.shift(delta, var)?) + } + ValueKind::NEOptionalLit(th) => { + ValueKind::NEOptionalLit(th.shift(delta, var)?) + } + ValueKind::EmptyListLit(tth) => { + ValueKind::EmptyListLit(tth.shift(delta, var)?) + } + ValueKind::NEListLit(elts) => { + ValueKind::NEListLit(elts.shift(delta, var)?) + } + ValueKind::RecordLit(kvs) => { + ValueKind::RecordLit(kvs.shift(delta, var)?) + } + ValueKind::RecordType(kvs) => { + ValueKind::RecordType(kvs.shift(delta, var)?) + } + ValueKind::UnionType(kts) => { + ValueKind::UnionType(kts.shift(delta, var)?) + } + ValueKind::UnionConstructor(x, kts) => { + ValueKind::UnionConstructor(x.clone(), kts.shift(delta, var)?) + } + ValueKind::UnionLit(x, v, kts) => ValueKind::UnionLit( + x.clone(), + v.shift(delta, var)?, + kts.shift(delta, var)?, + ), + ValueKind::TextLit(elts) => { + ValueKind::TextLit(elts.shift(delta, var)?) + } + ValueKind::Equivalence(x, y) => ValueKind::Equivalence( + x.shift(delta, var)?, + y.shift(delta, var)?, + ), + ValueKind::PartialExpr(e) => { + ValueKind::PartialExpr(e.shift(delta, var)?) + } + }) + } +} + impl Subst<Value> for Value { fn subst_shift(&self, var: &AlphaVar, val: &Value) -> Self { - match &*self.as_valuef() { + match &*self.as_kind() { // If the var matches, we can just reuse the provided value instead of copying it. // We also check that the types match, if in debug mode. - ValueF::Var(v) if v == var => { + ValueKind::Var(v) if v == var => { if let Ok(self_ty) = self.get_type() { val.check_type(&self_ty.subst_shift(var, val)); } @@ -303,13 +487,80 @@ impl Subst<Value> for ValueInternal { ValueInternal { // The resulting value may not stay in wnhf after substitution form: Unevaled, - value: self.value.subst_shift(var, val), + kind: self.kind.subst_shift(var, val), ty: self.ty.subst_shift(var, val), span: self.span.clone(), } } } +impl Subst<Value> for ValueKind { + fn subst_shift(&self, var: &AlphaVar, val: &Value) -> Self { + match self { + ValueKind::AppliedBuiltin(b, args) => { + ValueKind::AppliedBuiltin(*b, args.subst_shift(var, val)) + } + ValueKind::PartialExpr(e) => { + ValueKind::PartialExpr(e.subst_shift(var, val)) + } + ValueKind::TextLit(elts) => { + ValueKind::TextLit(elts.subst_shift(var, val)) + } + ValueKind::Lam(x, t, e) => ValueKind::Lam( + x.clone(), + t.subst_shift(var, val), + e.subst_shift(&var.under_binder(x), &val.under_binder(x)), + ), + ValueKind::Pi(x, t, e) => ValueKind::Pi( + x.clone(), + t.subst_shift(var, val), + e.subst_shift(&var.under_binder(x), &val.under_binder(x)), + ), + ValueKind::Var(v) if v == var => val.to_whnf_ignore_type(), + ValueKind::Var(v) => ValueKind::Var(v.shift(-1, var).unwrap()), + ValueKind::Const(c) => ValueKind::Const(*c), + ValueKind::BoolLit(b) => ValueKind::BoolLit(*b), + ValueKind::NaturalLit(n) => ValueKind::NaturalLit(*n), + ValueKind::IntegerLit(n) => ValueKind::IntegerLit(*n), + ValueKind::DoubleLit(n) => ValueKind::DoubleLit(*n), + ValueKind::EmptyOptionalLit(tth) => { + ValueKind::EmptyOptionalLit(tth.subst_shift(var, val)) + } + ValueKind::NEOptionalLit(th) => { + ValueKind::NEOptionalLit(th.subst_shift(var, val)) + } + ValueKind::EmptyListLit(tth) => { + ValueKind::EmptyListLit(tth.subst_shift(var, val)) + } + ValueKind::NEListLit(elts) => { + ValueKind::NEListLit(elts.subst_shift(var, val)) + } + ValueKind::RecordLit(kvs) => { + ValueKind::RecordLit(kvs.subst_shift(var, val)) + } + ValueKind::RecordType(kvs) => { + ValueKind::RecordType(kvs.subst_shift(var, val)) + } + ValueKind::UnionType(kts) => { + ValueKind::UnionType(kts.subst_shift(var, val)) + } + ValueKind::UnionConstructor(x, kts) => ValueKind::UnionConstructor( + x.clone(), + kts.subst_shift(var, val), + ), + ValueKind::UnionLit(x, v, kts) => ValueKind::UnionLit( + x.clone(), + v.subst_shift(var, val), + kts.subst_shift(var, val), + ), + ValueKind::Equivalence(x, y) => ValueKind::Equivalence( + x.subst_shift(var, val), + y.subst_shift(var, val), + ), + } + } +} + // TODO: use Rc comparison to shortcut on identical pointers impl std::cmp::PartialEq for Value { fn eq(&self, other: &Self) -> bool { @@ -321,11 +572,11 @@ impl std::cmp::Eq for Value {} impl std::fmt::Debug for Value { fn fmt(&self, fmt: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { let vint: &ValueInternal = &self.as_internal(); - if let ValueF::Const(c) = &vint.value { + if let ValueKind::Const(c) = &vint.kind { write!(fmt, "{:?}", c) } else { let mut x = fmt.debug_struct(&format!("Value@{:?}", &vint.form)); - x.field("value", &vint.value); + x.field("value", &vint.kind); if let Some(ty) = vint.ty.as_ref() { x.field("type", &ty); } else { diff --git a/dhall/src/semantics/core/valuef.rs b/dhall/src/semantics/core/valuef.rs deleted file mode 100644 index 73c715a..0000000 --- a/dhall/src/semantics/core/valuef.rs +++ /dev/null @@ -1,323 +0,0 @@ -use std::collections::HashMap; - -use crate::semantics::core::value::{ToExprOptions, Value}; -use crate::semantics::core::var::{AlphaLabel, AlphaVar, Shift, Subst}; -use crate::semantics::phase::typecheck::rc; -use crate::semantics::phase::{Normalized, NormalizedExpr}; -use crate::syntax; -use crate::syntax::{ - Builtin, Const, ExprF, Integer, InterpolatedTextContents, Label, - NaiveDouble, Natural, -}; - -/// A semantic value. Subexpressions are Values, which are partially evaluated expressions that are -/// normalized on-demand. -/// If you compare for equality two `ValueF`s in WHNF, then equality will be up to -/// alpha-equivalence (renaming of bound variables) and beta-equivalence (normalization). It will -/// recursively normalize as needed. -#[derive(Debug, Clone, PartialEq, Eq)] -pub(crate) enum ValueF { - /// Closures - Lam(AlphaLabel, Value, Value), - Pi(AlphaLabel, Value, Value), - // Invariant: in whnf, the evaluation must not be able to progress further. - AppliedBuiltin(Builtin, Vec<Value>), - - Var(AlphaVar), - Const(Const), - BoolLit(bool), - NaturalLit(Natural), - IntegerLit(Integer), - DoubleLit(NaiveDouble), - EmptyOptionalLit(Value), - NEOptionalLit(Value), - // EmptyListLit(t) means `[] : List t`, not `[] : t` - EmptyListLit(Value), - NEListLit(Vec<Value>), - RecordType(HashMap<Label, Value>), - RecordLit(HashMap<Label, Value>), - UnionType(HashMap<Label, Option<Value>>), - UnionConstructor(Label, HashMap<Label, Option<Value>>), - UnionLit(Label, Value, HashMap<Label, Option<Value>>), - // Invariant: in whnf, this must not contain interpolations that are themselves TextLits, and - // contiguous text values must be merged. - TextLit(Vec<InterpolatedTextContents<Value>>), - Equivalence(Value, Value), - // Invariant: in whnf, this must not contain a value captured by one of the variants above. - PartialExpr(ExprF<Value, Normalized>), -} - -impl ValueF { - pub(crate) fn into_value_with_type(self, t: Value) -> Value { - Value::from_valuef_and_type(self, t) - } - - pub(crate) fn to_expr(&self, opts: ToExprOptions) -> NormalizedExpr { - match self { - ValueF::Lam(x, t, e) => rc(ExprF::Lam( - x.to_label_maybe_alpha(opts.alpha), - t.to_expr(opts), - e.to_expr(opts), - )), - ValueF::AppliedBuiltin(b, args) => args - .iter() - .map(|v| v.to_expr(opts)) - .fold(rc(ExprF::Builtin(*b)), |acc, v| rc(ExprF::App(acc, v))), - ValueF::Pi(x, t, e) => rc(ExprF::Pi( - x.to_label_maybe_alpha(opts.alpha), - t.to_expr(opts), - e.to_expr(opts), - )), - ValueF::Var(v) => rc(ExprF::Var(v.to_var(opts.alpha))), - ValueF::Const(c) => rc(ExprF::Const(*c)), - ValueF::BoolLit(b) => rc(ExprF::BoolLit(*b)), - ValueF::NaturalLit(n) => rc(ExprF::NaturalLit(*n)), - ValueF::IntegerLit(n) => rc(ExprF::IntegerLit(*n)), - ValueF::DoubleLit(n) => rc(ExprF::DoubleLit(*n)), - ValueF::EmptyOptionalLit(n) => rc(ExprF::App( - rc(ExprF::Builtin(Builtin::OptionalNone)), - n.to_expr(opts), - )), - ValueF::NEOptionalLit(n) => rc(ExprF::SomeLit(n.to_expr(opts))), - ValueF::EmptyListLit(n) => rc(ExprF::EmptyListLit(rc(ExprF::App( - rc(ExprF::Builtin(Builtin::List)), - n.to_expr(opts), - )))), - ValueF::NEListLit(elts) => rc(ExprF::NEListLit( - elts.iter().map(|n| n.to_expr(opts)).collect(), - )), - ValueF::RecordLit(kvs) => rc(ExprF::RecordLit( - kvs.iter() - .map(|(k, v)| (k.clone(), v.to_expr(opts))) - .collect(), - )), - ValueF::RecordType(kts) => rc(ExprF::RecordType( - kts.iter() - .map(|(k, v)| (k.clone(), v.to_expr(opts))) - .collect(), - )), - ValueF::UnionType(kts) => rc(ExprF::UnionType( - kts.iter() - .map(|(k, v)| { - (k.clone(), v.as_ref().map(|v| v.to_expr(opts))) - }) - .collect(), - )), - ValueF::UnionConstructor(l, kts) => rc(ExprF::Field( - ValueF::UnionType(kts.clone()).to_expr(opts), - l.clone(), - )), - ValueF::UnionLit(l, v, kts) => rc(ExprF::App( - ValueF::UnionConstructor(l.clone(), kts.clone()).to_expr(opts), - v.to_expr(opts), - )), - ValueF::TextLit(elts) => rc(ExprF::TextLit( - elts.iter() - .map(|contents| contents.map_ref(|e| e.to_expr(opts))) - .collect(), - )), - ValueF::Equivalence(x, y) => rc(ExprF::BinOp( - syntax::BinOp::Equivalence, - x.to_expr(opts), - y.to_expr(opts), - )), - ValueF::PartialExpr(e) => rc(e.map_ref(|v| v.to_expr(opts))), - } - } - - pub(crate) fn normalize_mut(&mut self) { - match self { - ValueF::Var(_) - | ValueF::Const(_) - | ValueF::BoolLit(_) - | ValueF::NaturalLit(_) - | ValueF::IntegerLit(_) - | ValueF::DoubleLit(_) => {} - - ValueF::EmptyOptionalLit(tth) | ValueF::EmptyListLit(tth) => { - tth.normalize_mut(); - } - - ValueF::NEOptionalLit(th) => { - th.normalize_mut(); - } - ValueF::Lam(_, t, e) => { - t.normalize_mut(); - e.normalize_mut(); - } - ValueF::Pi(_, t, e) => { - t.normalize_mut(); - e.normalize_mut(); - } - ValueF::AppliedBuiltin(_, args) => { - for x in args.iter_mut() { - x.normalize_mut(); - } - } - ValueF::NEListLit(elts) => { - for x in elts.iter_mut() { - x.normalize_mut(); - } - } - ValueF::RecordLit(kvs) => { - for x in kvs.values_mut() { - x.normalize_mut(); - } - } - ValueF::RecordType(kvs) => { - for x in kvs.values_mut() { - x.normalize_mut(); - } - } - ValueF::UnionType(kts) | ValueF::UnionConstructor(_, kts) => { - for x in kts.values_mut().flat_map(|opt| opt) { - x.normalize_mut(); - } - } - ValueF::UnionLit(_, v, kts) => { - v.normalize_mut(); - for x in kts.values_mut().flat_map(|opt| opt) { - x.normalize_mut(); - } - } - ValueF::TextLit(elts) => { - for x in elts.iter_mut() { - x.map_mut(Value::normalize_mut); - } - } - ValueF::Equivalence(x, y) => { - x.normalize_mut(); - y.normalize_mut(); - } - ValueF::PartialExpr(e) => { - e.map_mut(Value::normalize_mut); - } - } - } - - pub(crate) fn from_builtin(b: Builtin) -> ValueF { - ValueF::AppliedBuiltin(b, vec![]) - } -} - -impl Shift for ValueF { - fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> { - Some(match self { - ValueF::Lam(x, t, e) => ValueF::Lam( - x.clone(), - t.shift(delta, var)?, - e.shift(delta, &var.under_binder(x))?, - ), - ValueF::AppliedBuiltin(b, args) => { - ValueF::AppliedBuiltin(*b, args.shift(delta, var)?) - } - ValueF::Pi(x, t, e) => ValueF::Pi( - x.clone(), - t.shift(delta, var)?, - e.shift(delta, &var.under_binder(x))?, - ), - ValueF::Var(v) => ValueF::Var(v.shift(delta, var)?), - ValueF::Const(c) => ValueF::Const(*c), - ValueF::BoolLit(b) => ValueF::BoolLit(*b), - ValueF::NaturalLit(n) => ValueF::NaturalLit(*n), - ValueF::IntegerLit(n) => ValueF::IntegerLit(*n), - ValueF::DoubleLit(n) => ValueF::DoubleLit(*n), - ValueF::EmptyOptionalLit(tth) => { - ValueF::EmptyOptionalLit(tth.shift(delta, var)?) - } - ValueF::NEOptionalLit(th) => { - ValueF::NEOptionalLit(th.shift(delta, var)?) - } - ValueF::EmptyListLit(tth) => { - ValueF::EmptyListLit(tth.shift(delta, var)?) - } - ValueF::NEListLit(elts) => { - ValueF::NEListLit(elts.shift(delta, var)?) - } - ValueF::RecordLit(kvs) => ValueF::RecordLit(kvs.shift(delta, var)?), - ValueF::RecordType(kvs) => { - ValueF::RecordType(kvs.shift(delta, var)?) - } - ValueF::UnionType(kts) => ValueF::UnionType(kts.shift(delta, var)?), - ValueF::UnionConstructor(x, kts) => { - ValueF::UnionConstructor(x.clone(), kts.shift(delta, var)?) - } - ValueF::UnionLit(x, v, kts) => ValueF::UnionLit( - x.clone(), - v.shift(delta, var)?, - kts.shift(delta, var)?, - ), - ValueF::TextLit(elts) => ValueF::TextLit(elts.shift(delta, var)?), - ValueF::Equivalence(x, y) => { - ValueF::Equivalence(x.shift(delta, var)?, y.shift(delta, var)?) - } - ValueF::PartialExpr(e) => ValueF::PartialExpr(e.shift(delta, var)?), - }) - } -} - -impl Subst<Value> for ValueF { - fn subst_shift(&self, var: &AlphaVar, val: &Value) -> Self { - match self { - ValueF::AppliedBuiltin(b, args) => { - ValueF::AppliedBuiltin(*b, args.subst_shift(var, val)) - } - ValueF::PartialExpr(e) => { - ValueF::PartialExpr(e.subst_shift(var, val)) - } - ValueF::TextLit(elts) => { - ValueF::TextLit(elts.subst_shift(var, val)) - } - ValueF::Lam(x, t, e) => ValueF::Lam( - x.clone(), - t.subst_shift(var, val), - e.subst_shift(&var.under_binder(x), &val.under_binder(x)), - ), - ValueF::Pi(x, t, e) => ValueF::Pi( - x.clone(), - t.subst_shift(var, val), - e.subst_shift(&var.under_binder(x), &val.under_binder(x)), - ), - ValueF::Var(v) if v == var => val.to_whnf_ignore_type(), - ValueF::Var(v) => ValueF::Var(v.shift(-1, var).unwrap()), - ValueF::Const(c) => ValueF::Const(*c), - ValueF::BoolLit(b) => ValueF::BoolLit(*b), - ValueF::NaturalLit(n) => ValueF::NaturalLit(*n), - ValueF::IntegerLit(n) => ValueF::IntegerLit(*n), - ValueF::DoubleLit(n) => ValueF::DoubleLit(*n), - ValueF::EmptyOptionalLit(tth) => { - ValueF::EmptyOptionalLit(tth.subst_shift(var, val)) - } - ValueF::NEOptionalLit(th) => { - ValueF::NEOptionalLit(th.subst_shift(var, val)) - } - ValueF::EmptyListLit(tth) => { - ValueF::EmptyListLit(tth.subst_shift(var, val)) - } - ValueF::NEListLit(elts) => { - ValueF::NEListLit(elts.subst_shift(var, val)) - } - ValueF::RecordLit(kvs) => { - ValueF::RecordLit(kvs.subst_shift(var, val)) - } - ValueF::RecordType(kvs) => { - ValueF::RecordType(kvs.subst_shift(var, val)) - } - ValueF::UnionType(kts) => { - ValueF::UnionType(kts.subst_shift(var, val)) - } - ValueF::UnionConstructor(x, kts) => { - ValueF::UnionConstructor(x.clone(), kts.subst_shift(var, val)) - } - ValueF::UnionLit(x, v, kts) => ValueF::UnionLit( - x.clone(), - v.subst_shift(var, val), - kts.subst_shift(var, val), - ), - ValueF::Equivalence(x, y) => ValueF::Equivalence( - x.subst_shift(var, val), - y.subst_shift(var, val), - ), - } - } -} diff --git a/dhall/src/semantics/core/var.rs b/dhall/src/semantics/core/var.rs index 184a372..1548713 100644 --- a/dhall/src/semantics/core/var.rs +++ b/dhall/src/semantics/core/var.rs @@ -1,6 +1,6 @@ use std::collections::HashMap; -use crate::syntax::{ExprF, InterpolatedTextContents, Label, V}; +use crate::syntax::{ExprKind, InterpolatedTextContents, Label, V}; /// Stores a pair of variables: a normal one and one /// that corresponds to the alpha-normalized version of the first one. @@ -12,7 +12,7 @@ pub struct AlphaVar { } // Exactly like a Label, but equality returns always true. -// This is so that ValueF equality is exactly alpha-equivalence. +// This is so that ValueKind equality is exactly alpha-equivalence. #[derive(Clone, Eq)] pub struct AlphaLabel(Label); @@ -190,7 +190,7 @@ impl<T: Shift> Shift for std::cell::RefCell<T> { } } -impl<T: Shift, E: Clone> Shift for ExprF<T, E> { +impl<T: Shift, E: Clone> Shift for ExprKind<T, E> { fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> { Some(self.traverse_ref_with_special_handling_of_binders( |v| Ok(v.shift(delta, var)?), @@ -262,7 +262,7 @@ impl<S, T: Subst<S>> Subst<S> for std::cell::RefCell<T> { } } -impl<S: Shift, T: Subst<S>, E: Clone> Subst<S> for ExprF<T, E> { +impl<S: Shift, T: Subst<S>, E: Clone> Subst<S> for ExprKind<T, E> { fn subst_shift(&self, var: &AlphaVar, val: &S) -> Self { self.map_ref_with_special_handling_of_binders( |v| v.subst_shift(var, val), diff --git a/dhall/src/semantics/mod.rs b/dhall/src/semantics/mod.rs index 9d2e462..1eeef86 100644 --- a/dhall/src/semantics/mod.rs +++ b/dhall/src/semantics/mod.rs @@ -1,3 +1,3 @@ pub mod core; -pub mod error; pub mod phase; +pub mod to_expr; diff --git a/dhall/src/semantics/phase/mod.rs b/dhall/src/semantics/phase/mod.rs index 752c257..b22120d 100644 --- a/dhall/src/semantics/phase/mod.rs +++ b/dhall/src/semantics/phase/mod.rs @@ -1,10 +1,11 @@ use std::fmt::Display; use std::path::Path; -use crate::semantics::core::value::{ToExprOptions, Value}; -use crate::semantics::core::valuef::ValueF; +use crate::error::{EncodeError, Error, ImportError, TypeError}; +use crate::semantics::core::value::Value; +use crate::semantics::core::value::ValueKind; use crate::semantics::core::var::{AlphaVar, Shift, Subst}; -use crate::semantics::error::{EncodeError, Error, ImportError, TypeError}; +use crate::semantics::to_expr::ToExprOptions; use crate::syntax::binary; use crate::syntax::{Builtin, Const, Expr}; use resolve::ImportRoot; @@ -76,13 +77,6 @@ impl Resolved { impl Typed { /// Reduce an expression to its normal form, performing beta reduction - /// - /// `normalize` does not type-check the expression. You may want to type-check - /// expressions before normalizing them since normalization can convert an - /// ill-typed expression into a well-typed expression. - /// - /// However, `normalize` will not fail if the expression is ill-typed and will - /// leave ill-typed sub-expressions unevaluated. pub fn normalize(mut self) -> Normalized { self.normalize_mut(); Normalized(self) @@ -91,8 +85,8 @@ impl Typed { pub(crate) fn from_const(c: Const) -> Self { Typed(Value::from_const(c)) } - pub(crate) fn from_valuef_and_type(v: ValueF, t: Typed) -> Self { - Typed(Value::from_valuef_and_type(v, t.into_value())) + pub(crate) fn from_kind_and_type(v: ValueKind, t: Typed) -> Self { + Typed(Value::from_kind_and_type(v, t.into_value())) } pub(crate) fn from_value(th: Value) -> Self { Typed(th) @@ -101,18 +95,22 @@ impl Typed { Typed::from_const(Const::Type) } + /// Converts a value back to the corresponding AST expression. pub(crate) fn to_expr(&self) -> NormalizedExpr { self.0.to_expr(ToExprOptions { alpha: false, normalize: false, }) } + /// Converts a value back to the corresponding AST expression, beta-normalizing in the process. pub fn normalize_to_expr(&self) -> NormalizedExpr { self.0.to_expr(ToExprOptions { alpha: false, normalize: true, }) } + /// Converts a value back to the corresponding AST expression, (alpha,beta)-normalizing in the + /// process. pub(crate) fn normalize_to_expr_alpha(&self) -> NormalizedExpr { self.0.to_expr(ToExprOptions { alpha: true, @@ -148,8 +146,8 @@ impl Typed { pub fn make_record_type( kts: impl Iterator<Item = (String, Typed)>, ) -> Self { - Typed::from_valuef_and_type( - ValueF::RecordType( + Typed::from_kind_and_type( + ValueKind::RecordType( kts.map(|(k, t)| (k.into(), t.into_value())).collect(), ), Typed::const_type(), @@ -158,8 +156,8 @@ impl Typed { pub fn make_union_type( kts: impl Iterator<Item = (String, Option<Typed>)>, ) -> Self { - Typed::from_valuef_and_type( - ValueF::UnionType( + Typed::from_kind_and_type( + ValueKind::UnionType( kts.map(|(k, t)| (k.into(), t.map(|t| t.into_value()))) .collect(), ), diff --git a/dhall/src/semantics/phase/normalize.rs b/dhall/src/semantics/phase/normalize.rs index 81c3ce1..d81a910 100644 --- a/dhall/src/semantics/phase/normalize.rs +++ b/dhall/src/semantics/phase/normalize.rs @@ -1,14 +1,14 @@ use std::collections::HashMap; use crate::semantics::core::value::Value; -use crate::semantics::core::valuef::ValueF; +use crate::semantics::core::value::ValueKind; use crate::semantics::core::var::{AlphaLabel, AlphaVar, Shift, Subst}; use crate::semantics::phase::Normalized; use crate::syntax; use crate::syntax::Const::Type; use crate::syntax::{ - BinOp, Builtin, ExprF, InterpolatedText, InterpolatedTextContents, Label, - NaiveDouble, + BinOp, Builtin, ExprKind, InterpolatedText, InterpolatedTextContents, + Label, NaiveDouble, }; // Ad-hoc macro to help construct closures @@ -19,7 +19,7 @@ macro_rules! make_closure { Label::from(stringify!($var)).into(), $n ); - ValueF::Var(var) + ValueKind::Var(var) .into_value_with_type(make_closure!($($ty)*)) }}; // Warning: assumes that $ty, as a dhall value, has type `Type` @@ -28,9 +28,9 @@ macro_rules! make_closure { let ty = make_closure!($($ty)*); let body = make_closure!($($body)*); let body_ty = body.get_type_not_sort(); - let lam_ty = ValueF::Pi(var.clone(), ty.clone(), body_ty) + let lam_ty = ValueKind::Pi(var.clone(), ty.clone(), body_ty) .into_value_with_type(Value::from_const(Type)); - ValueF::Lam(var, ty, body).into_value_with_type(lam_ty) + ValueKind::Lam(var, ty, body).into_value_with_type(lam_ty) }}; (Natural) => { Value::from_builtin(Builtin::Natural) @@ -43,14 +43,14 @@ macro_rules! make_closure { let v = make_closure!($($rest)*); let v_type = v.get_type_not_sort(); let opt_v_type = Value::from_builtin(Builtin::Optional).app(v_type); - ValueF::NEOptionalLit(v).into_value_with_type(opt_v_type) + ValueKind::NEOptionalLit(v).into_value_with_type(opt_v_type) }}; (1 + $($rest:tt)*) => { - ValueF::PartialExpr(ExprF::BinOp( + ValueKind::PartialExpr(ExprKind::BinOp( syntax::BinOp::NaturalPlus, make_closure!($($rest)*), - Value::from_valuef_and_type( - ValueF::NaturalLit(1), + Value::from_kind_and_type( + ValueKind::NaturalLit(1), make_closure!(Natural) ), )).into_value_with_type( @@ -61,9 +61,9 @@ macro_rules! make_closure { let head = make_closure!($($head)*); let tail = make_closure!($($tail)*); let list_type = tail.get_type_not_sort(); - ValueF::PartialExpr(ExprF::BinOp( + ValueKind::PartialExpr(ExprKind::BinOp( syntax::BinOp::ListAppend, - ValueF::NEListLit(vec![head]) + ValueKind::NEListLit(vec![head]) .into_value_with_type(list_type.clone()), tail, )).into_value_with_type(list_type) @@ -75,13 +75,13 @@ pub(crate) fn apply_builtin( b: Builtin, args: Vec<Value>, ty: &Value, -) -> ValueF { +) -> ValueKind { use syntax::Builtin::*; - use ValueF::*; + use ValueKind::*; // Small helper enum enum Ret<'a> { - ValueF(ValueF), + ValueKind(ValueKind), Value(Value), // For applications that can return a function, it's important to keep the remaining // arguments to apply them to the resulting function. @@ -90,38 +90,38 @@ pub(crate) fn apply_builtin( } let ret = match (b, args.as_slice()) { - (OptionalNone, [t]) => Ret::ValueF(EmptyOptionalLit(t.clone())), + (OptionalNone, [t]) => Ret::ValueKind(EmptyOptionalLit(t.clone())), (NaturalIsZero, [n]) => match &*n.as_whnf() { - NaturalLit(n) => Ret::ValueF(BoolLit(*n == 0)), + NaturalLit(n) => Ret::ValueKind(BoolLit(*n == 0)), _ => Ret::DoneAsIs, }, (NaturalEven, [n]) => match &*n.as_whnf() { - NaturalLit(n) => Ret::ValueF(BoolLit(*n % 2 == 0)), + NaturalLit(n) => Ret::ValueKind(BoolLit(*n % 2 == 0)), _ => Ret::DoneAsIs, }, (NaturalOdd, [n]) => match &*n.as_whnf() { - NaturalLit(n) => Ret::ValueF(BoolLit(*n % 2 != 0)), + NaturalLit(n) => Ret::ValueKind(BoolLit(*n % 2 != 0)), _ => Ret::DoneAsIs, }, (NaturalToInteger, [n]) => match &*n.as_whnf() { - NaturalLit(n) => Ret::ValueF(IntegerLit(*n as isize)), + NaturalLit(n) => Ret::ValueKind(IntegerLit(*n as isize)), _ => Ret::DoneAsIs, }, - (NaturalShow, [n]) => match &*n.as_whnf() { - NaturalLit(n) => { - Ret::ValueF(TextLit(vec![InterpolatedTextContents::Text( - n.to_string(), - )])) + (NaturalShow, [n]) => { + match &*n.as_whnf() { + NaturalLit(n) => Ret::ValueKind(TextLit(vec![ + InterpolatedTextContents::Text(n.to_string()), + ])), + _ => Ret::DoneAsIs, } - _ => Ret::DoneAsIs, - }, + } (NaturalSubtract, [a, b]) => match (&*a.as_whnf(), &*b.as_whnf()) { (NaturalLit(a), NaturalLit(b)) => { - Ret::ValueF(NaturalLit(if b > a { b - a } else { 0 })) + Ret::ValueKind(NaturalLit(if b > a { b - a } else { 0 })) } (NaturalLit(0), _) => Ret::Value(b.clone()), - (_, NaturalLit(0)) => Ret::ValueF(NaturalLit(0)), - _ if a == b => Ret::ValueF(NaturalLit(0)), + (_, NaturalLit(0)) => Ret::ValueKind(NaturalLit(0)), + _ if a == b => Ret::ValueKind(NaturalLit(0)), _ => Ret::DoneAsIs, }, (IntegerShow, [n]) => match &*n.as_whnf() { @@ -131,24 +131,24 @@ pub(crate) fn apply_builtin( } else { format!("+{}", n) }; - Ret::ValueF(TextLit(vec![InterpolatedTextContents::Text(s)])) + Ret::ValueKind(TextLit(vec![InterpolatedTextContents::Text(s)])) } _ => Ret::DoneAsIs, }, (IntegerToDouble, [n]) => match &*n.as_whnf() { IntegerLit(n) => { - Ret::ValueF(DoubleLit(NaiveDouble::from(*n as f64))) + Ret::ValueKind(DoubleLit(NaiveDouble::from(*n as f64))) } _ => Ret::DoneAsIs, }, - (DoubleShow, [n]) => match &*n.as_whnf() { - DoubleLit(n) => { - Ret::ValueF(TextLit(vec![InterpolatedTextContents::Text( - n.to_string(), - )])) + (DoubleShow, [n]) => { + match &*n.as_whnf() { + DoubleLit(n) => Ret::ValueKind(TextLit(vec![ + InterpolatedTextContents::Text(n.to_string()), + ])), + _ => Ret::DoneAsIs, } - _ => Ret::DoneAsIs, - }, + } (TextShow, [v]) => match &*v.as_whnf() { TextLit(elts) => { match elts.as_slice() { @@ -158,7 +158,7 @@ pub(crate) fn apply_builtin( let txt: InterpolatedText<Normalized> = std::iter::empty().collect(); let s = txt.to_string(); - Ret::ValueF(TextLit(vec![ + Ret::ValueKind(TextLit(vec![ InterpolatedTextContents::Text(s), ])) } @@ -172,7 +172,7 @@ pub(crate) fn apply_builtin( )) .collect(); let s = txt.to_string(); - Ret::ValueF(TextLit(vec![ + Ret::ValueKind(TextLit(vec![ InterpolatedTextContents::Text(s), ])) } @@ -182,28 +182,28 @@ pub(crate) fn apply_builtin( _ => Ret::DoneAsIs, }, (ListLength, [_, l]) => match &*l.as_whnf() { - EmptyListLit(_) => Ret::ValueF(NaturalLit(0)), - NEListLit(xs) => Ret::ValueF(NaturalLit(xs.len())), + EmptyListLit(_) => Ret::ValueKind(NaturalLit(0)), + NEListLit(xs) => Ret::ValueKind(NaturalLit(xs.len())), _ => Ret::DoneAsIs, }, (ListHead, [_, l]) => match &*l.as_whnf() { - EmptyListLit(n) => Ret::ValueF(EmptyOptionalLit(n.clone())), + EmptyListLit(n) => Ret::ValueKind(EmptyOptionalLit(n.clone())), NEListLit(xs) => { - Ret::ValueF(NEOptionalLit(xs.iter().next().unwrap().clone())) + Ret::ValueKind(NEOptionalLit(xs.iter().next().unwrap().clone())) } _ => Ret::DoneAsIs, }, (ListLast, [_, l]) => match &*l.as_whnf() { - EmptyListLit(n) => Ret::ValueF(EmptyOptionalLit(n.clone())), - NEListLit(xs) => Ret::ValueF(NEOptionalLit( + EmptyListLit(n) => Ret::ValueKind(EmptyOptionalLit(n.clone())), + NEListLit(xs) => Ret::ValueKind(NEOptionalLit( xs.iter().rev().next().unwrap().clone(), )), _ => Ret::DoneAsIs, }, (ListReverse, [_, l]) => match &*l.as_whnf() { - EmptyListLit(n) => Ret::ValueF(EmptyListLit(n.clone())), + EmptyListLit(n) => Ret::ValueKind(EmptyListLit(n.clone())), NEListLit(xs) => { - Ret::ValueF(NEListLit(xs.iter().rev().cloned().collect())) + Ret::ValueKind(NEListLit(xs.iter().rev().cloned().collect())) } _ => Ret::DoneAsIs, }, @@ -222,7 +222,7 @@ pub(crate) fn apply_builtin( let mut kts = HashMap::new(); kts.insert("index".into(), Value::from_builtin(Natural)); kts.insert("value".into(), t.clone()); - let t = Value::from_valuef_and_type( + let t = Value::from_kind_and_type( RecordType(kts), Value::from_const(Type), ); @@ -237,7 +237,7 @@ pub(crate) fn apply_builtin( let mut kvs = HashMap::new(); kvs.insert( "index".into(), - Value::from_valuef_and_type( + Value::from_kind_and_type( NaturalLit(i), Value::from_builtin( Builtin::Natural, @@ -245,7 +245,7 @@ pub(crate) fn apply_builtin( ), ); kvs.insert("value".into(), e.clone()); - Value::from_valuef_and_type( + Value::from_kind_and_type( RecordLit(kvs), t.clone(), ) @@ -254,14 +254,14 @@ pub(crate) fn apply_builtin( ), _ => unreachable!(), }; - Ret::ValueF(list) + Ret::ValueKind(list) } _ => Ret::DoneAsIs, } } (ListBuild, [t, f]) => match &*f.as_whnf() { // fold/build fusion - ValueF::AppliedBuiltin(ListFold, args) => { + ValueKind::AppliedBuiltin(ListFold, args) => { if args.len() >= 2 { Ret::Value(args[1].clone()) } else { @@ -303,7 +303,7 @@ pub(crate) fn apply_builtin( }, (OptionalBuild, [t, f]) => match &*f.as_whnf() { // fold/build fusion - ValueF::AppliedBuiltin(OptionalFold, args) => { + ValueKind::AppliedBuiltin(OptionalFold, args) => { if args.len() >= 2 { Ret::Value(args[1].clone()) } else { @@ -338,7 +338,7 @@ pub(crate) fn apply_builtin( }, (NaturalBuild, [f]) => match &*f.as_whnf() { // fold/build fusion - ValueF::AppliedBuiltin(NaturalFold, args) => { + ValueKind::AppliedBuiltin(NaturalFold, args) => { if !args.is_empty() { Ret::Value(args[0].clone()) } else { @@ -375,7 +375,7 @@ pub(crate) fn apply_builtin( _ => Ret::DoneAsIs, }; match ret { - Ret::ValueF(v) => v, + Ret::ValueKind(v) => v, Ret::Value(v) => v.to_whnf_check_type(ty), Ret::ValueWithRemainingArgs(unconsumed_args, mut v) => { let n_consumed_args = args.len() - unconsumed_args.len(); @@ -388,23 +388,23 @@ pub(crate) fn apply_builtin( } } -pub(crate) fn apply_any(f: Value, a: Value, ty: &Value) -> ValueF { +pub(crate) fn apply_any(f: Value, a: Value, ty: &Value) -> ValueKind { let f_borrow = f.as_whnf(); match &*f_borrow { - ValueF::Lam(x, _, e) => { + ValueKind::Lam(x, _, e) => { e.subst_shift(&x.into(), &a).to_whnf_check_type(ty) } - ValueF::AppliedBuiltin(b, args) => { + ValueKind::AppliedBuiltin(b, args) => { use std::iter::once; let args = args.iter().cloned().chain(once(a.clone())).collect(); apply_builtin(*b, args, ty) } - ValueF::UnionConstructor(l, kts) => { - ValueF::UnionLit(l.clone(), a, kts.clone()) + ValueKind::UnionConstructor(l, kts) => { + ValueKind::UnionLit(l.clone(), a, kts.clone()) } _ => { drop(f_borrow); - ValueF::PartialExpr(ExprF::App(f, a)) + ValueKind::PartialExpr(ExprKind::App(f, a)) } } } @@ -426,7 +426,7 @@ pub(crate) fn squash_textlit( Expr(e) => { let e_borrow = e.as_whnf(); match &*e_borrow { - ValueF::TextLit(elts2) => { + ValueKind::TextLit(elts2) => { inner(elts2.iter().cloned(), crnt_str, ret) } _ => { @@ -479,10 +479,10 @@ where // Small helper enum to avoid repetition enum Ret<'a> { - ValueF(ValueF), + ValueKind(ValueKind), Value(Value), ValueRef(&'a Value), - Expr(ExprF<Value, Normalized>), + Expr(ExprKind<Value, Normalized>), } fn apply_binop<'a>( @@ -496,7 +496,7 @@ fn apply_binop<'a>( NaturalTimes, RecursiveRecordMerge, RecursiveRecordTypeMerge, RightBiasedRecordMerge, TextAppend, }; - use ValueF::{ + use ValueKind::{ BoolLit, EmptyListLit, NEListLit, NaturalLit, RecordLit, RecordType, TextLit, }; @@ -505,58 +505,58 @@ fn apply_binop<'a>( Some(match (o, &*x_borrow, &*y_borrow) { (BoolAnd, BoolLit(true), _) => Ret::ValueRef(y), (BoolAnd, _, BoolLit(true)) => Ret::ValueRef(x), - (BoolAnd, BoolLit(false), _) => Ret::ValueF(BoolLit(false)), - (BoolAnd, _, BoolLit(false)) => Ret::ValueF(BoolLit(false)), + (BoolAnd, BoolLit(false), _) => Ret::ValueKind(BoolLit(false)), + (BoolAnd, _, BoolLit(false)) => Ret::ValueKind(BoolLit(false)), (BoolAnd, _, _) if x == y => Ret::ValueRef(x), - (BoolOr, BoolLit(true), _) => Ret::ValueF(BoolLit(true)), - (BoolOr, _, BoolLit(true)) => Ret::ValueF(BoolLit(true)), + (BoolOr, BoolLit(true), _) => Ret::ValueKind(BoolLit(true)), + (BoolOr, _, BoolLit(true)) => Ret::ValueKind(BoolLit(true)), (BoolOr, BoolLit(false), _) => Ret::ValueRef(y), (BoolOr, _, BoolLit(false)) => Ret::ValueRef(x), (BoolOr, _, _) if x == y => Ret::ValueRef(x), (BoolEQ, BoolLit(true), _) => Ret::ValueRef(y), (BoolEQ, _, BoolLit(true)) => Ret::ValueRef(x), - (BoolEQ, BoolLit(x), BoolLit(y)) => Ret::ValueF(BoolLit(x == y)), - (BoolEQ, _, _) if x == y => Ret::ValueF(BoolLit(true)), + (BoolEQ, BoolLit(x), BoolLit(y)) => Ret::ValueKind(BoolLit(x == y)), + (BoolEQ, _, _) if x == y => Ret::ValueKind(BoolLit(true)), (BoolNE, BoolLit(false), _) => Ret::ValueRef(y), (BoolNE, _, BoolLit(false)) => Ret::ValueRef(x), - (BoolNE, BoolLit(x), BoolLit(y)) => Ret::ValueF(BoolLit(x != y)), - (BoolNE, _, _) if x == y => Ret::ValueF(BoolLit(false)), + (BoolNE, BoolLit(x), BoolLit(y)) => Ret::ValueKind(BoolLit(x != y)), + (BoolNE, _, _) if x == y => Ret::ValueKind(BoolLit(false)), (NaturalPlus, NaturalLit(0), _) => Ret::ValueRef(y), (NaturalPlus, _, NaturalLit(0)) => Ret::ValueRef(x), (NaturalPlus, NaturalLit(x), NaturalLit(y)) => { - Ret::ValueF(NaturalLit(x + y)) + Ret::ValueKind(NaturalLit(x + y)) } - (NaturalTimes, NaturalLit(0), _) => Ret::ValueF(NaturalLit(0)), - (NaturalTimes, _, NaturalLit(0)) => Ret::ValueF(NaturalLit(0)), + (NaturalTimes, NaturalLit(0), _) => Ret::ValueKind(NaturalLit(0)), + (NaturalTimes, _, NaturalLit(0)) => Ret::ValueKind(NaturalLit(0)), (NaturalTimes, NaturalLit(1), _) => Ret::ValueRef(y), (NaturalTimes, _, NaturalLit(1)) => Ret::ValueRef(x), (NaturalTimes, NaturalLit(x), NaturalLit(y)) => { - Ret::ValueF(NaturalLit(x * y)) + Ret::ValueKind(NaturalLit(x * y)) } (ListAppend, EmptyListLit(_), _) => Ret::ValueRef(y), (ListAppend, _, EmptyListLit(_)) => Ret::ValueRef(x), - (ListAppend, NEListLit(xs), NEListLit(ys)) => Ret::ValueF(NEListLit( - xs.iter().chain(ys.iter()).cloned().collect(), - )), + (ListAppend, NEListLit(xs), NEListLit(ys)) => Ret::ValueKind( + NEListLit(xs.iter().chain(ys.iter()).cloned().collect()), + ), (TextAppend, TextLit(x), _) if x.is_empty() => Ret::ValueRef(y), (TextAppend, _, TextLit(y)) if y.is_empty() => Ret::ValueRef(x), - (TextAppend, TextLit(x), TextLit(y)) => Ret::ValueF(TextLit( + (TextAppend, TextLit(x), TextLit(y)) => Ret::ValueKind(TextLit( squash_textlit(x.iter().chain(y.iter()).cloned()), )), (TextAppend, TextLit(x), _) => { use std::iter::once; let y = InterpolatedTextContents::Expr(y.clone()); - Ret::ValueF(TextLit(squash_textlit( + Ret::ValueKind(TextLit(squash_textlit( x.iter().cloned().chain(once(y)), ))) } (TextAppend, _, TextLit(y)) => { use std::iter::once; let x = InterpolatedTextContents::Expr(x.clone()); - Ret::ValueF(TextLit(squash_textlit( + Ret::ValueKind(TextLit(squash_textlit( once(x).chain(y.iter().cloned()), ))) } @@ -573,7 +573,7 @@ fn apply_binop<'a>( // Insert only if key not already present kvs.entry(x.clone()).or_insert_with(|| v.clone()); } - Ret::ValueF(RecordLit(kvs)) + Ret::ValueKind(RecordLit(kvs)) } (RecursiveRecordMerge, _, RecordLit(kvs)) if kvs.is_empty() => { @@ -589,8 +589,8 @@ fn apply_binop<'a>( _ => unreachable!("Internal type error"), }; let kvs = merge_maps::<_, _, _, !>(kvs1, kvs2, |k, v1, v2| { - Ok(Value::from_valuef_and_type( - ValueF::PartialExpr(ExprF::BinOp( + Ok(Value::from_kind_and_type( + ValueKind::PartialExpr(ExprKind::BinOp( RecursiveRecordMerge, v1.clone(), v2.clone(), @@ -598,7 +598,7 @@ fn apply_binop<'a>( kts.get(k).expect("Internal type error").clone(), )) })?; - Ret::ValueF(RecordLit(kvs)) + Ret::ValueKind(RecordLit(kvs)) } (RecursiveRecordTypeMerge, _, _) | (Equivalence, _, _) => { @@ -610,46 +610,46 @@ fn apply_binop<'a>( } pub(crate) fn normalize_one_layer( - expr: ExprF<Value, Normalized>, + expr: ExprKind<Value, Normalized>, ty: &Value, -) -> ValueF { - use ValueF::{ +) -> ValueKind { + use ValueKind::{ AppliedBuiltin, BoolLit, DoubleLit, EmptyListLit, IntegerLit, NEListLit, NEOptionalLit, NaturalLit, RecordLit, TextLit, UnionConstructor, UnionLit, UnionType, }; let ret = match expr { - ExprF::Import(_) => unreachable!( + ExprKind::Import(_) => unreachable!( "There should remain no imports in a resolved expression" ), // Those cases have already been completely handled in the typechecking phase (using // `RetWhole`), so they won't appear here. - ExprF::Lam(_, _, _) - | ExprF::Pi(_, _, _) - | ExprF::Let(_, _, _, _) - | ExprF::Embed(_) - | ExprF::Const(_) - | ExprF::Builtin(_) - | ExprF::Var(_) - | ExprF::Annot(_, _) - | ExprF::RecordType(_) - | ExprF::UnionType(_) => { + ExprKind::Lam(_, _, _) + | ExprKind::Pi(_, _, _) + | ExprKind::Let(_, _, _, _) + | ExprKind::Embed(_) + | ExprKind::Const(_) + | ExprKind::Builtin(_) + | ExprKind::Var(_) + | ExprKind::Annot(_, _) + | ExprKind::RecordType(_) + | ExprKind::UnionType(_) => { unreachable!("This case should have been handled in typecheck") } - ExprF::Assert(_) => Ret::Expr(expr), - ExprF::App(v, a) => Ret::Value(v.app(a)), - ExprF::BoolLit(b) => Ret::ValueF(BoolLit(b)), - ExprF::NaturalLit(n) => Ret::ValueF(NaturalLit(n)), - ExprF::IntegerLit(n) => Ret::ValueF(IntegerLit(n)), - ExprF::DoubleLit(n) => Ret::ValueF(DoubleLit(n)), - ExprF::SomeLit(e) => Ret::ValueF(NEOptionalLit(e)), - ExprF::EmptyListLit(ref t) => { + ExprKind::Assert(_) => Ret::Expr(expr), + ExprKind::App(v, a) => Ret::Value(v.app(a)), + ExprKind::BoolLit(b) => Ret::ValueKind(BoolLit(b)), + ExprKind::NaturalLit(n) => Ret::ValueKind(NaturalLit(n)), + ExprKind::IntegerLit(n) => Ret::ValueKind(IntegerLit(n)), + ExprKind::DoubleLit(n) => Ret::ValueKind(DoubleLit(n)), + ExprKind::SomeLit(e) => Ret::ValueKind(NEOptionalLit(e)), + ExprKind::EmptyListLit(ref t) => { // Check if the type is of the form `List x` let t_borrow = t.as_whnf(); match &*t_borrow { AppliedBuiltin(Builtin::List, args) if args.len() == 1 => { - Ret::ValueF(EmptyListLit(args[0].clone())) + Ret::ValueKind(EmptyListLit(args[0].clone())) } _ => { drop(t_borrow); @@ -657,23 +657,23 @@ pub(crate) fn normalize_one_layer( } } } - ExprF::NEListLit(elts) => { - Ret::ValueF(NEListLit(elts.into_iter().collect())) + ExprKind::NEListLit(elts) => { + Ret::ValueKind(NEListLit(elts.into_iter().collect())) } - ExprF::RecordLit(kvs) => { - Ret::ValueF(RecordLit(kvs.into_iter().collect())) + ExprKind::RecordLit(kvs) => { + Ret::ValueKind(RecordLit(kvs.into_iter().collect())) } - ExprF::TextLit(elts) => { + ExprKind::TextLit(elts) => { use InterpolatedTextContents::Expr; let elts: Vec<_> = squash_textlit(elts.into_iter()); // Simplify bare interpolation if let [Expr(th)] = elts.as_slice() { Ret::Value(th.clone()) } else { - Ret::ValueF(TextLit(elts)) + Ret::ValueKind(TextLit(elts)) } } - ExprF::BoolIf(ref b, ref e1, ref e2) => { + ExprKind::BoolIf(ref b, ref e1, ref e2) => { let b_borrow = b.as_whnf(); match &*b_borrow { BoolLit(true) => Ret::ValueRef(e1), @@ -695,18 +695,18 @@ pub(crate) fn normalize_one_layer( } } } - ExprF::BinOp(o, ref x, ref y) => match apply_binop(o, x, y, ty) { + ExprKind::BinOp(o, ref x, ref y) => match apply_binop(o, x, y, ty) { Some(ret) => ret, None => Ret::Expr(expr), }, - ExprF::Projection(_, ref ls) if ls.is_empty() => { - Ret::ValueF(RecordLit(HashMap::new())) + ExprKind::Projection(_, ref ls) if ls.is_empty() => { + Ret::ValueKind(RecordLit(HashMap::new())) } - ExprF::Projection(ref v, ref ls) => { + ExprKind::Projection(ref v, ref ls) => { let v_borrow = v.as_whnf(); match &*v_borrow { - RecordLit(kvs) => Ret::ValueF(RecordLit( + RecordLit(kvs) => Ret::ValueKind(RecordLit( ls.iter() .filter_map(|l| { kvs.get(l).map(|x| (l.clone(), x.clone())) @@ -719,7 +719,7 @@ pub(crate) fn normalize_one_layer( } } } - ExprF::Field(ref v, ref l) => { + ExprKind::Field(ref v, ref l) => { let v_borrow = v.as_whnf(); match &*v_borrow { RecordLit(kvs) => match kvs.get(l) { @@ -730,7 +730,7 @@ pub(crate) fn normalize_one_layer( } }, UnionType(kts) => { - Ret::ValueF(UnionConstructor(l.clone(), kts.clone())) + Ret::ValueKind(UnionConstructor(l.clone(), kts.clone())) } _ => { drop(v_borrow); @@ -738,11 +738,11 @@ pub(crate) fn normalize_one_layer( } } } - ExprF::ProjectionByExpr(_, _) => { + ExprKind::ProjectionByExpr(_, _) => { unimplemented!("selection by expression") } - ExprF::Merge(ref handlers, ref variant, _) => { + ExprKind::Merge(ref handlers, ref variant, _) => { let handlers_borrow = handlers.as_whnf(); let variant_borrow = variant.as_whnf(); match (&*handlers_borrow, &*variant_borrow) { @@ -769,24 +769,24 @@ pub(crate) fn normalize_one_layer( } } } - ExprF::ToMap(_, _) => unimplemented!("toMap"), + ExprKind::ToMap(_, _) => unimplemented!("toMap"), }; match ret { - Ret::ValueF(v) => v, + Ret::ValueKind(v) => v, Ret::Value(v) => v.to_whnf_check_type(ty), Ret::ValueRef(v) => v.to_whnf_check_type(ty), - Ret::Expr(expr) => ValueF::PartialExpr(expr), + Ret::Expr(expr) => ValueKind::PartialExpr(expr), } } -/// Normalize a ValueF into WHNF -pub(crate) fn normalize_whnf(v: ValueF, ty: &Value) -> ValueF { +/// Normalize a ValueKind into WHNF +pub(crate) fn normalize_whnf(v: ValueKind, ty: &Value) -> ValueKind { match v { - ValueF::AppliedBuiltin(b, args) => apply_builtin(b, args, ty), - ValueF::PartialExpr(e) => normalize_one_layer(e, ty), - ValueF::TextLit(elts) => { - ValueF::TextLit(squash_textlit(elts.into_iter())) + ValueKind::AppliedBuiltin(b, args) => apply_builtin(b, args, ty), + ValueKind::PartialExpr(e) => normalize_one_layer(e, ty), + ValueKind::TextLit(elts) => { + ValueKind::TextLit(squash_textlit(elts.into_iter())) } // All other cases are already in WHNF v => v, diff --git a/dhall/src/semantics/phase/parse.rs b/dhall/src/semantics/phase/parse.rs index 4c8ad7b..00db422 100644 --- a/dhall/src/semantics/phase/parse.rs +++ b/dhall/src/semantics/phase/parse.rs @@ -2,7 +2,7 @@ use std::fs::File; use std::io::Read; use std::path::Path; -use crate::semantics::error::Error; +use crate::error::Error; use crate::semantics::phase::resolve::ImportRoot; use crate::semantics::phase::Parsed; use crate::syntax::binary; diff --git a/dhall/src/semantics/phase/resolve.rs b/dhall/src/semantics/phase/resolve.rs index 86dc7ae..cc4a024 100644 --- a/dhall/src/semantics/phase/resolve.rs +++ b/dhall/src/semantics/phase/resolve.rs @@ -1,7 +1,7 @@ use std::collections::HashMap; use std::path::{Path, PathBuf}; -use crate::semantics::error::{Error, ImportError}; +use crate::error::{Error, ImportError}; use crate::semantics::phase::{Normalized, NormalizedExpr, Parsed, Resolved}; use crate::syntax; use crate::syntax::{FilePath, ImportLocation, URL}; diff --git a/dhall/src/semantics/phase/typecheck.rs b/dhall/src/semantics/phase/typecheck.rs index 59380a3..c439f74 100644 --- a/dhall/src/semantics/phase/typecheck.rs +++ b/dhall/src/semantics/phase/typecheck.rs @@ -1,16 +1,17 @@ use std::cmp::max; use std::collections::HashMap; +use crate::error::{TypeError, TypeMessage}; use crate::semantics::core::context::TypecheckContext; use crate::semantics::core::value::Value; -use crate::semantics::core::valuef::ValueF; +use crate::semantics::core::value::ValueKind; use crate::semantics::core::var::{Shift, Subst}; -use crate::semantics::error::{TypeError, TypeMessage}; use crate::semantics::phase::normalize::merge_maps; use crate::semantics::phase::Normalized; use crate::syntax; use crate::syntax::{ - Builtin, Const, Expr, ExprF, InterpolatedTextContents, Label, RawExpr, Span, + Builtin, Const, Expr, ExprKind, InterpolatedTextContents, Label, Span, + UnspannedExpr, }; fn tck_pi_type( @@ -39,8 +40,8 @@ fn tck_pi_type( let k = function_check(ka, kb); - Ok(Value::from_valuef_and_type( - ValueF::Pi(x.into(), tx, te), + Ok(Value::from_kind_and_type( + ValueKind::Pi(x.into(), tx, te), Value::from_const(k), )) } @@ -71,8 +72,8 @@ fn tck_record_type( }; } - Ok(Value::from_valuef_and_type( - ValueF::RecordType(new_kts), + Ok(Value::from_kind_and_type( + ValueKind::RecordType(new_kts), Value::from_const(k), )) } @@ -116,8 +117,8 @@ where // an union type with only unary variants also has type Type let k = k.unwrap_or(Const::Type); - Ok(Value::from_valuef_and_type( - ValueF::UnionType(new_kts), + Ok(Value::from_kind_and_type( + ValueKind::UnionType(new_kts), Value::from_const(k), )) } @@ -131,42 +132,42 @@ fn function_check(a: Const, b: Const) -> Const { } pub(crate) fn const_to_value(c: Const) -> Value { - let v = ValueF::Const(c); + let v = ValueKind::Const(c); match c { Const::Type => { - Value::from_valuef_and_type(v, const_to_value(Const::Kind)) + Value::from_kind_and_type(v, const_to_value(Const::Kind)) } Const::Kind => { - Value::from_valuef_and_type(v, const_to_value(Const::Sort)) + Value::from_kind_and_type(v, const_to_value(Const::Sort)) } Const::Sort => Value::const_sort(), } } -pub fn rc<E>(x: RawExpr<E>) -> Expr<E> { +pub fn rc<E>(x: UnspannedExpr<E>) -> Expr<E> { Expr::new(x, Span::Artificial) } // Ad-hoc macro to help construct the types of builtins macro_rules! make_type { - (Type) => { ExprF::Const(Const::Type) }; - (Bool) => { ExprF::Builtin(Builtin::Bool) }; - (Natural) => { ExprF::Builtin(Builtin::Natural) }; - (Integer) => { ExprF::Builtin(Builtin::Integer) }; - (Double) => { ExprF::Builtin(Builtin::Double) }; - (Text) => { ExprF::Builtin(Builtin::Text) }; + (Type) => { ExprKind::Const(Const::Type) }; + (Bool) => { ExprKind::Builtin(Builtin::Bool) }; + (Natural) => { ExprKind::Builtin(Builtin::Natural) }; + (Integer) => { ExprKind::Builtin(Builtin::Integer) }; + (Double) => { ExprKind::Builtin(Builtin::Double) }; + (Text) => { ExprKind::Builtin(Builtin::Text) }; ($var:ident) => { - ExprF::Var(syntax::V(stringify!($var).into(), 0)) + ExprKind::Var(syntax::V(stringify!($var).into(), 0)) }; (Optional $ty:ident) => { - ExprF::App( - rc(ExprF::Builtin(Builtin::Optional)), + ExprKind::App( + rc(ExprKind::Builtin(Builtin::Optional)), rc(make_type!($ty)) ) }; (List $($rest:tt)*) => { - ExprF::App( - rc(ExprF::Builtin(Builtin::List)), + ExprKind::App( + rc(ExprKind::Builtin(Builtin::List)), rc(make_type!($($rest)*)) ) }; @@ -178,24 +179,24 @@ macro_rules! make_type { rc(make_type!($ty)), ); )* - ExprF::RecordType(kts) + ExprKind::RecordType(kts) }}; ($ty:ident -> $($rest:tt)*) => { - ExprF::Pi( + ExprKind::Pi( "_".into(), rc(make_type!($ty)), rc(make_type!($($rest)*)) ) }; (($($arg:tt)*) -> $($rest:tt)*) => { - ExprF::Pi( + ExprKind::Pi( "_".into(), rc(make_type!($($arg)*)), rc(make_type!($($rest)*)) ) }; (forall ($var:ident : $($ty:tt)*) -> $($rest:tt)*) => { - ExprF::Pi( + ExprKind::Pi( stringify!($var).into(), rc(make_type!($($ty)*)), rc(make_type!($($rest)*)) @@ -290,8 +291,8 @@ fn type_of_builtin<E>(b: Builtin) -> Expr<E> { pub(crate) fn builtin_to_value(b: Builtin) -> Value { let ctx = TypecheckContext::new(); - Value::from_valuef_and_type( - ValueF::from_builtin(b), + Value::from_kind_and_type( + ValueKind::from_builtin(b), type_with(&ctx, type_of_builtin(b)).unwrap(), ) } @@ -304,7 +305,7 @@ fn type_with( ctx: &TypecheckContext, e: Expr<Normalized>, ) -> Result<Value, TypeError> { - use syntax::ExprF::{Annot, Embed, Lam, Let, Pi, Var}; + use syntax::ExprKind::{Annot, Embed, Lam, Let, Pi, Var}; let span = e.span(); Ok(match e.as_ref() { @@ -313,8 +314,8 @@ fn type_with( let ctx2 = ctx.insert_type(var, annot.clone()); let body = type_with(&ctx2, body.clone())?; let body_type = body.get_type()?; - Value::from_valuef_and_type( - ValueF::Lam(var.clone().into(), annot.clone(), body), + Value::from_kind_and_type( + ValueKind::Lam(var.clone().into(), annot.clone(), body), tck_pi_type(ctx, var.clone(), annot, body_type)?, ) } @@ -359,13 +360,13 @@ fn type_with( /// layer. fn type_last_layer( ctx: &TypecheckContext, - e: ExprF<Value, Normalized>, + e: ExprKind<Value, Normalized>, span: Span, ) -> Result<Value, TypeError> { use syntax::BinOp::*; use syntax::Builtin::*; use syntax::Const::Type; - use syntax::ExprF::*; + use syntax::ExprKind::*; use TypeMessage::*; let mkerr = |msg: TypeMessage| Err(TypeError::new(ctx, msg)); @@ -389,7 +390,7 @@ fn type_last_layer( let tf = f.get_type()?; let tf_borrow = tf.as_whnf(); let (x, tx, tb) = match &*tf_borrow { - ValueF::Pi(x, tx, tb) => (x, tx, tb), + ValueKind::Pi(x, tx, tb) => (x, tx, tb), _ => return mkerr(NotAFunction(f.clone())), }; if &a.get_type()? != tx { @@ -406,8 +407,8 @@ fn type_last_layer( } Assert(t) => { match &*t.as_whnf() { - ValueF::Equivalence(x, y) if x == y => {} - ValueF::Equivalence(x, y) => { + ValueKind::Equivalence(x, y) if x == y => {} + ValueKind::Equivalence(x, y) => { return mkerr(AssertMismatch(x.clone(), y.clone())) } _ => return mkerr(AssertMustTakeEquivalence), @@ -415,7 +416,7 @@ fn type_last_layer( RetTypeOnly(t.clone()) } BoolIf(x, y, z) => { - if *x.get_type()?.as_whnf() != ValueF::from_builtin(Bool) { + if *x.get_type()?.as_whnf() != ValueKind::from_builtin(Bool) { return mkerr(InvalidPredicate(x.clone())); } @@ -435,7 +436,7 @@ fn type_last_layer( } EmptyListLit(t) => { match &*t.as_whnf() { - ValueF::AppliedBuiltin(syntax::Builtin::List, args) + ValueKind::AppliedBuiltin(syntax::Builtin::List, args) if args.len() == 1 => {} _ => return mkerr(InvalidListType(t.clone())), } @@ -482,7 +483,7 @@ fn type_last_layer( )?), Field(r, x) => { match &*r.get_type()?.as_whnf() { - ValueF::RecordType(kts) => match kts.get(&x) { + ValueKind::RecordType(kts) => match kts.get(&x) { Some(tth) => { RetTypeOnly(tth.clone()) }, @@ -492,7 +493,7 @@ fn type_last_layer( // TODO: branch here only when r.get_type() is a Const _ => { match &*r.as_whnf() { - ValueF::UnionType(kts) => match kts.get(&x) { + ValueKind::UnionType(kts) => match kts.get(&x) { // Constructor has type T -> < x: T, ... > Some(Some(t)) => { RetTypeOnly( @@ -553,14 +554,14 @@ fn type_last_layer( // Extract the LHS record type let l_type_borrow = l_type.as_whnf(); let kts_x = match &*l_type_borrow { - ValueF::RecordType(kts) => kts, + ValueKind::RecordType(kts) => kts, _ => return mkerr(MustCombineRecord(l.clone())), }; // Extract the RHS record type let r_type_borrow = r_type.as_whnf(); let kts_y = match &*r_type_borrow { - ValueF::RecordType(kts) => kts, + ValueKind::RecordType(kts) => kts, _ => return mkerr(MustCombineRecord(r.clone())), }; @@ -578,7 +579,7 @@ fn type_last_layer( } BinOp(RecursiveRecordMerge, l, r) => RetTypeOnly(type_last_layer( ctx, - ExprF::BinOp( + ExprKind::BinOp( RecursiveRecordTypeMerge, l.get_type()?, r.get_type()?, @@ -589,7 +590,7 @@ fn type_last_layer( // Extract the LHS record type let borrow_l = l.as_whnf(); let kts_x = match &*borrow_l { - ValueF::RecordType(kts) => kts, + ValueKind::RecordType(kts) => kts, _ => { return mkerr(RecordTypeMergeRequiresRecordType(l.clone())) } @@ -598,7 +599,7 @@ fn type_last_layer( // Extract the RHS record type let borrow_r = r.as_whnf(); let kts_y = match &*borrow_r { - ValueF::RecordType(kts) => kts, + ValueKind::RecordType(kts) => kts, _ => { return mkerr(RecordTypeMergeRequiresRecordType(r.clone())) } @@ -612,7 +613,7 @@ fn type_last_layer( |_, l: &Value, r: &Value| { type_last_layer( ctx, - ExprF::BinOp( + ExprKind::BinOp( RecursiveRecordTypeMerge, l.clone(), r.clone(), @@ -626,7 +627,7 @@ fn type_last_layer( } BinOp(o @ ListAppend, l, r) => { match &*l.get_type()?.as_whnf() { - ValueF::AppliedBuiltin(List, _) => {} + ValueKind::AppliedBuiltin(List, _) => {} _ => return mkerr(BinOpTypeMismatch(*o, l.clone())), } @@ -648,8 +649,8 @@ fn type_last_layer( return mkerr(EquivalenceTypeMismatch(r.clone(), l.clone())); } - RetWhole(Value::from_valuef_and_type( - ValueF::Equivalence(l.clone(), r.clone()), + RetWhole(Value::from_kind_and_type( + ValueKind::Equivalence(l.clone(), r.clone()), Value::from_const(Type), )) } @@ -684,14 +685,14 @@ fn type_last_layer( let record_type = record.get_type()?; let record_borrow = record_type.as_whnf(); let handlers = match &*record_borrow { - ValueF::RecordType(kts) => kts, + ValueKind::RecordType(kts) => kts, _ => return mkerr(Merge1ArgMustBeRecord(record.clone())), }; let union_type = union.get_type()?; let union_borrow = union_type.as_whnf(); let variants = match &*union_borrow { - ValueF::UnionType(kts) => kts, + ValueKind::UnionType(kts) => kts, _ => return mkerr(Merge2ArgMustBeUnion(union.clone())), }; @@ -703,7 +704,7 @@ fn type_last_layer( Some(Some(variant_type)) => { let handler_type_borrow = handler_type.as_whnf(); let (x, tx, tb) = match &*handler_type_borrow { - ValueF::Pi(x, tx, tb) => (x, tx, tb), + ValueKind::Pi(x, tx, tb) => (x, tx, tb), _ => { return mkerr(NotAFunction( handler_type.clone(), @@ -765,7 +766,7 @@ fn type_last_layer( let record_type = record.get_type()?; let record_type_borrow = record_type.as_whnf(); let kts = match &*record_type_borrow { - ValueF::RecordType(kts) => kts, + ValueKind::RecordType(kts) => kts, _ => return mkerr(ProjectionMustBeRecord), }; @@ -777,8 +778,8 @@ fn type_last_layer( }; } - RetTypeOnly(Value::from_valuef_and_type( - ValueF::RecordType(new_kts), + RetTypeOnly(Value::from_kind_and_type( + ValueKind::RecordType(new_kts), record_type.get_type()?, )) } @@ -786,8 +787,8 @@ fn type_last_layer( }; Ok(match ret { - RetTypeOnly(typ) => Value::from_valuef_and_type_and_span( - ValueF::PartialExpr(e), + RetTypeOnly(typ) => Value::from_kind_and_type_and_span( + ValueKind::PartialExpr(e), typ, span, ), @@ -806,5 +807,5 @@ pub(crate) fn typecheck_with( expr: Expr<Normalized>, ty: Expr<Normalized>, ) -> Result<Value, TypeError> { - typecheck(expr.rewrap(ExprF::Annot(expr.clone(), ty))) + typecheck(expr.rewrap(ExprKind::Annot(expr.clone(), ty))) } diff --git a/dhall/src/semantics/to_expr.rs b/dhall/src/semantics/to_expr.rs new file mode 100644 index 0000000..b21fb29 --- /dev/null +++ b/dhall/src/semantics/to_expr.rs @@ -0,0 +1,105 @@ +use crate::semantics::core::value::Value; +use crate::semantics::core::value::ValueKind; +use crate::semantics::phase::typecheck::rc; +use crate::semantics::phase::NormalizedExpr; +use crate::syntax; +use crate::syntax::{Builtin, ExprKind}; + +#[derive(Copy, Clone)] +/// Controls conversion from `Value` to `Expr` +pub(crate) struct ToExprOptions { + /// Whether to convert all variables to `_` + pub(crate) alpha: bool, + /// Whether to normalize before converting + pub(crate) normalize: bool, +} + +/// Converts a value back to the corresponding AST expression. +pub(crate) fn value_to_expr( + val: &Value, + opts: ToExprOptions, +) -> NormalizedExpr { + if opts.normalize { + val.normalize_whnf(); + } + val.as_kind().to_expr(opts) +} + +/// Converts a value back to the corresponding AST expression. +pub(crate) fn kind_to_expr( + kind: &ValueKind, + opts: ToExprOptions, +) -> NormalizedExpr { + match kind { + ValueKind::Lam(x, t, e) => rc(ExprKind::Lam( + x.to_label_maybe_alpha(opts.alpha), + t.to_expr(opts), + e.to_expr(opts), + )), + ValueKind::AppliedBuiltin(b, args) => args + .iter() + .map(|v| v.to_expr(opts)) + .fold(rc(ExprKind::Builtin(*b)), |acc, v| { + rc(ExprKind::App(acc, v)) + }), + ValueKind::Pi(x, t, e) => rc(ExprKind::Pi( + x.to_label_maybe_alpha(opts.alpha), + t.to_expr(opts), + e.to_expr(opts), + )), + ValueKind::Var(v) => rc(ExprKind::Var(v.to_var(opts.alpha))), + ValueKind::Const(c) => rc(ExprKind::Const(*c)), + ValueKind::BoolLit(b) => rc(ExprKind::BoolLit(*b)), + ValueKind::NaturalLit(n) => rc(ExprKind::NaturalLit(*n)), + ValueKind::IntegerLit(n) => rc(ExprKind::IntegerLit(*n)), + ValueKind::DoubleLit(n) => rc(ExprKind::DoubleLit(*n)), + ValueKind::EmptyOptionalLit(n) => rc(ExprKind::App( + rc(ExprKind::Builtin(Builtin::OptionalNone)), + n.to_expr(opts), + )), + ValueKind::NEOptionalLit(n) => rc(ExprKind::SomeLit(n.to_expr(opts))), + ValueKind::EmptyListLit(n) => { + rc(ExprKind::EmptyListLit(rc(ExprKind::App( + rc(ExprKind::Builtin(Builtin::List)), + n.to_expr(opts), + )))) + } + ValueKind::NEListLit(elts) => rc(ExprKind::NEListLit( + elts.iter().map(|n| n.to_expr(opts)).collect(), + )), + ValueKind::RecordLit(kvs) => rc(ExprKind::RecordLit( + kvs.iter() + .map(|(k, v)| (k.clone(), v.to_expr(opts))) + .collect(), + )), + ValueKind::RecordType(kts) => rc(ExprKind::RecordType( + kts.iter() + .map(|(k, v)| (k.clone(), v.to_expr(opts))) + .collect(), + )), + ValueKind::UnionType(kts) => rc(ExprKind::UnionType( + kts.iter() + .map(|(k, v)| (k.clone(), v.as_ref().map(|v| v.to_expr(opts)))) + .collect(), + )), + ValueKind::UnionConstructor(l, kts) => rc(ExprKind::Field( + ValueKind::UnionType(kts.clone()).to_expr(opts), + l.clone(), + )), + ValueKind::UnionLit(l, v, kts) => rc(ExprKind::App( + ValueKind::UnionConstructor(l.clone(), kts.clone()).to_expr(opts), + v.to_expr(opts), + )), + ValueKind::TextLit(elts) => rc(ExprKind::TextLit( + elts.iter() + .map(|contents| contents.map_ref(|e| e.to_expr(opts))) + .collect(), + )), + ValueKind::Equivalence(x, y) => rc(ExprKind::BinOp( + syntax::BinOp::Equivalence, + x.to_expr(opts), + y.to_expr(opts), + )), + ValueKind::PartialExpr(e) => rc(e.map_ref(|v| v.to_expr(opts))), + } +} diff --git a/dhall/src/syntax/core/expr.rs b/dhall/src/syntax/ast/expr.rs index 5b9f401..48c48d8 100644 --- a/dhall/src/syntax/core/expr.rs +++ b/dhall/src/syntax/ast/expr.rs @@ -1,51 +1,15 @@ use crate::syntax::map::{DupTreeMap, DupTreeSet}; -use crate::syntax::visitor::{self, ExprFMutVisitor, ExprFVisitor}; +use crate::syntax::visitor::{self, ExprKindMutVisitor, ExprKindVisitor}; use crate::syntax::*; pub type Integer = isize; pub type Natural = usize; pub type Double = NaiveDouble; -pub fn trivial_result<T>(x: Result<T, !>) -> T { - match x { - Ok(x) => x, - Err(e) => e, - } -} - /// Double with bitwise equality #[derive(Debug, Copy, Clone)] pub struct NaiveDouble(f64); -impl PartialEq for NaiveDouble { - fn eq(&self, other: &Self) -> bool { - self.0.to_bits() == other.0.to_bits() - } -} - -impl Eq for NaiveDouble {} - -impl std::hash::Hash for NaiveDouble { - fn hash<H>(&self, state: &mut H) - where - H: std::hash::Hasher, - { - self.0.to_bits().hash(state) - } -} - -impl From<f64> for NaiveDouble { - fn from(x: f64) -> Self { - NaiveDouble(x) - } -} - -impl From<NaiveDouble> for f64 { - fn from(x: NaiveDouble) -> f64 { - x.0 - } -} - /// Constants for a pure type system #[derive(Debug, Copy, Clone, PartialEq, Eq, PartialOrd, Ord, Hash)] pub enum Const { @@ -62,18 +26,6 @@ pub enum Const { #[derive(Debug, Clone, PartialEq, Eq, Hash)] pub struct V<Label>(pub Label, pub usize); -// This is only for the specific `Label` type, not generic -impl From<Label> for V<Label> { - fn from(x: Label) -> V<Label> { - V(x, 0) - } -} -impl<'a> From<&'a Label> for V<Label> { - fn from(x: &'a Label) -> V<Label> { - V(x.clone(), 0) - } -} - // Definition order must match precedence order for // pretty-printing to work correctly #[derive(Debug, Copy, Clone, PartialEq, Eq, PartialOrd, Ord, Hash)] @@ -142,33 +94,19 @@ pub enum Builtin { // Each node carries an annotation. #[derive(Debug, Clone)] -pub struct Expr<Embed>(Box<(RawExpr<Embed>, Span)>); - -pub type RawExpr<Embed> = ExprF<Expr<Embed>, Embed>; - -impl<Embed: PartialEq> std::cmp::PartialEq for Expr<Embed> { - fn eq(&self, other: &Self) -> bool { - self.0.as_ref().0 == other.0.as_ref().0 - } +pub struct Expr<Embed> { + kind: Box<ExprKind<Expr<Embed>, Embed>>, + span: Span, } -impl<Embed: Eq> std::cmp::Eq for Expr<Embed> {} - -impl<Embed: std::hash::Hash> std::hash::Hash for Expr<Embed> { - fn hash<H>(&self, state: &mut H) - where - H: std::hash::Hasher, - { - (self.0).0.hash(state) - } -} +pub type UnspannedExpr<Embed> = ExprKind<Expr<Embed>, Embed>; /// Syntax tree for expressions // Having the recursion out of the enum definition enables writing // much more generic code and improves pattern-matching behind // smart pointers. #[derive(Debug, Clone, PartialEq, Eq, Hash)] -pub enum ExprF<SubExpr, Embed> { +pub enum ExprKind<SubExpr, Embed> { Const(Const), /// `x` /// `x@n` @@ -231,12 +169,12 @@ pub enum ExprF<SubExpr, Embed> { Embed(Embed), } -impl<SE, E> ExprF<SE, E> { +impl<SE, E> ExprKind<SE, E> { pub fn traverse_ref_with_special_handling_of_binders<'a, SE2, Err>( &'a self, visit_subexpr: impl FnMut(&'a SE) -> Result<SE2, Err>, visit_under_binder: impl FnOnce(&'a Label, &'a SE) -> Result<SE2, Err>, - ) -> Result<ExprF<SE2, E>, Err> + ) -> Result<ExprKind<SE2, E>, Err> where E: Clone, { @@ -250,7 +188,7 @@ impl<SE, E> ExprF<SE, E> { fn traverse_ref<'a, SE2, Err>( &'a self, visit_subexpr: impl FnMut(&'a SE) -> Result<SE2, Err>, - ) -> Result<ExprF<SE2, E>, Err> + ) -> Result<ExprKind<SE2, E>, Err> where E: Clone, { @@ -268,7 +206,7 @@ impl<SE, E> ExprF<SE, E> { &'a self, mut map_subexpr: impl FnMut(&'a SE) -> SE2, mut map_under_binder: impl FnMut(&'a Label, &'a SE) -> SE2, - ) -> ExprF<SE2, E> + ) -> ExprKind<SE2, E> where E: Clone, { @@ -281,7 +219,7 @@ impl<SE, E> ExprF<SE, E> { pub fn map_ref<'a, SE2>( &'a self, mut map_subexpr: impl FnMut(&'a SE) -> SE2, - ) -> ExprF<SE2, E> + ) -> ExprKind<SE2, E> where E: Clone, { @@ -294,22 +232,25 @@ impl<SE, E> ExprF<SE, E> { } impl<E> Expr<E> { - pub fn as_ref(&self) -> &RawExpr<E> { - &self.0.as_ref().0 - } - pub fn as_mut(&mut self) -> &mut RawExpr<E> { - &mut self.0.as_mut().0 + pub fn as_ref(&self) -> &UnspannedExpr<E> { + &self.kind } pub fn span(&self) -> Span { - self.0.as_ref().1.clone() + self.span.clone() } - pub fn new(x: RawExpr<E>, n: Span) -> Self { - Expr(Box::new((x, n))) + pub fn new(kind: UnspannedExpr<E>, span: Span) -> Self { + Expr { + kind: Box::new(kind), + span, + } } - pub fn rewrap<E2>(&self, x: RawExpr<E2>) -> Expr<E2> { - Expr(Box::new((x, (self.0).1.clone()))) + pub fn rewrap<E2>(&self, kind: UnspannedExpr<E2>) -> Expr<E2> { + Expr { + kind: Box::new(kind), + span: self.span.clone(), + } } pub fn traverse_resolve_mut<Err, F1>( @@ -320,21 +261,21 @@ impl<E> Expr<E> { E: Clone, F1: FnMut(Import<Expr<E>>) -> Result<E, Err>, { - match self.as_mut() { - ExprF::BinOp(BinOp::ImportAlt, l, r) => { - let garbage_expr = ExprF::BoolLit(false); + match self.kind.as_mut() { + ExprKind::BinOp(BinOp::ImportAlt, l, r) => { + let garbage_expr = ExprKind::BoolLit(false); let new_self = if l.traverse_resolve_mut(f).is_ok() { l } else { r.traverse_resolve_mut(f)?; r }; - *self.as_mut() = - std::mem::replace(new_self.as_mut(), garbage_expr); + *self.kind = + std::mem::replace(new_self.kind.as_mut(), garbage_expr); } _ => { - self.as_mut().traverse_mut(|e| e.traverse_resolve_mut(f))?; - if let ExprF::Import(import) = self.as_mut() { + self.kind.traverse_mut(|e| e.traverse_resolve_mut(f))?; + if let ExprKind::Import(import) = self.kind.as_mut() { let garbage_import = Import { mode: ImportMode::Code, location: ImportLocation::Missing, @@ -342,7 +283,7 @@ impl<E> Expr<E> { }; // Move out of &mut import let import = std::mem::replace(import, garbage_import); - *self.as_mut() = ExprF::Embed(f(import)?); + *self.kind = ExprKind::Embed(f(import)?); } } } @@ -350,16 +291,6 @@ impl<E> Expr<E> { } } -/// Add an isize to an usize -/// Returns `None` on over/underflow -fn add_ui(u: usize, i: isize) -> Option<usize> { - Some(if i < 0 { - u.checked_sub(i.checked_neg()? as usize)? - } else { - u.checked_add(i as usize)? - }) -} - impl<Label: PartialEq + Clone> V<Label> { pub fn shift(&self, delta: isize, var: &V<Label>) -> Option<Self> { let V(x, n) = var; @@ -375,3 +306,73 @@ impl<Label: PartialEq + Clone> V<Label> { self.shift(-1, &V(x.clone(), 0)) } } + +pub fn trivial_result<T>(x: Result<T, !>) -> T { + match x { + Ok(x) => x, + Err(e) => e, + } +} + +/// Add an isize to an usize +/// Returns `None` on over/underflow +fn add_ui(u: usize, i: isize) -> Option<usize> { + Some(if i < 0 { + u.checked_sub(i.checked_neg()? as usize)? + } else { + u.checked_add(i as usize)? + }) +} + +impl PartialEq for NaiveDouble { + fn eq(&self, other: &Self) -> bool { + self.0.to_bits() == other.0.to_bits() + } +} + +impl Eq for NaiveDouble {} + +impl std::hash::Hash for NaiveDouble { + fn hash<H>(&self, state: &mut H) + where + H: std::hash::Hasher, + { + self.0.to_bits().hash(state) + } +} + +impl From<f64> for NaiveDouble { + fn from(x: f64) -> Self { + NaiveDouble(x) + } +} + +impl From<NaiveDouble> for f64 { + fn from(x: NaiveDouble) -> f64 { + x.0 + } +} + +/// This is only for the specific `Label` type, not generic +impl From<Label> for V<Label> { + fn from(x: Label) -> V<Label> { + V(x, 0) + } +} + +impl<Embed: PartialEq> std::cmp::PartialEq for Expr<Embed> { + fn eq(&self, other: &Self) -> bool { + self.kind == other.kind + } +} + +impl<Embed: Eq> std::cmp::Eq for Expr<Embed> {} + +impl<Embed: std::hash::Hash> std::hash::Hash for Expr<Embed> { + fn hash<H>(&self, state: &mut H) + where + H: std::hash::Hasher, + { + self.kind.hash(state) + } +} diff --git a/dhall/src/syntax/core/import.rs b/dhall/src/syntax/ast/import.rs index da3e99b..da3e99b 100644 --- a/dhall/src/syntax/core/import.rs +++ b/dhall/src/syntax/ast/import.rs diff --git a/dhall/src/syntax/core/label.rs b/dhall/src/syntax/ast/label.rs index 43c3f53..43c3f53 100644 --- a/dhall/src/syntax/core/label.rs +++ b/dhall/src/syntax/ast/label.rs diff --git a/dhall/src/syntax/core/map.rs b/dhall/src/syntax/ast/map.rs index c4c6126..c4c6126 100644 --- a/dhall/src/syntax/core/map.rs +++ b/dhall/src/syntax/ast/map.rs diff --git a/dhall/src/syntax/core/mod.rs b/dhall/src/syntax/ast/mod.rs index 66bf229..1950154 100644 --- a/dhall/src/syntax/core/mod.rs +++ b/dhall/src/syntax/ast/mod.rs @@ -8,6 +8,5 @@ mod span; pub use span::*; mod text; pub use text::*; -pub mod context; pub mod map; pub mod visitor; diff --git a/dhall/src/syntax/core/span.rs b/dhall/src/syntax/ast/span.rs index f9c7008..f9c7008 100644 --- a/dhall/src/syntax/core/span.rs +++ b/dhall/src/syntax/ast/span.rs diff --git a/dhall/src/syntax/core/text.rs b/dhall/src/syntax/ast/text.rs index fb390ee..fb390ee 100644 --- a/dhall/src/syntax/core/text.rs +++ b/dhall/src/syntax/ast/text.rs diff --git a/dhall/src/syntax/core/visitor.rs b/dhall/src/syntax/ast/visitor.rs index b76d037..b557995 100644 --- a/dhall/src/syntax/core/visitor.rs +++ b/dhall/src/syntax/ast/visitor.rs @@ -1,7 +1,7 @@ use crate::syntax::*; use std::iter::FromIterator; -/// A visitor trait that can be used to traverse `ExprF`s. We need this pattern so that Rust lets +/// A visitor trait that can be used to traverse `ExprKind`s. We need this pattern so that Rust lets /// us have as much mutability as we can. /// For example, `traverse_ref_with_special_handling_of_binders` cannot be made using only /// `traverse_ref`, because `traverse_ref` takes a `FnMut` so we would need to pass multiple @@ -9,7 +9,7 @@ use std::iter::FromIterator; /// preventing exactly this ! So we have to be more clever. The visitor pattern allows us to have /// only one mutable thing the whole time: the visitor itself. The visitor can then carry around /// multiple closures or just one, and Rust is ok with either. See for example TraverseRefVisitor. -pub trait ExprFVisitor<'a, SE1, SE2, E1, E2>: Sized { +pub trait ExprKindVisitor<'a, SE1, SE2, E1, E2>: Sized { type Error; fn visit_subexpr(&mut self, subexpr: &'a SE1) -> Result<SE2, Self::Error>; @@ -25,14 +25,14 @@ pub trait ExprFVisitor<'a, SE1, SE2, E1, E2>: Sized { fn visit( self, - input: &'a ExprF<SE1, E1>, - ) -> Result<ExprF<SE2, E2>, Self::Error> { + input: &'a ExprKind<SE1, E1>, + ) -> Result<ExprKind<SE2, E2>, Self::Error> { visit_ref(self, input) } } -/// Like `ExprFVisitor`, but by mutable reference -pub trait ExprFMutVisitor<'a, SE, E>: Sized { +/// Like `ExprKindVisitor`, but by mutable reference +pub trait ExprKindMutVisitor<'a, SE, E>: Sized { type Error; fn visit_subexpr(&mut self, subexpr: &'a mut SE) @@ -49,17 +49,17 @@ pub trait ExprFMutVisitor<'a, SE, E>: Sized { self.visit_subexpr(subexpr) } - fn visit(self, input: &'a mut ExprF<SE, E>) -> Result<(), Self::Error> { + fn visit(self, input: &'a mut ExprKind<SE, E>) -> Result<(), Self::Error> { visit_mut(self, input) } } fn visit_ref<'a, V, SE1, SE2, E1, E2>( mut v: V, - input: &'a ExprF<SE1, E1>, -) -> Result<ExprF<SE2, E2>, V::Error> + input: &'a ExprKind<SE1, E1>, +) -> Result<ExprKind<SE2, E2>, V::Error> where - V: ExprFVisitor<'a, SE1, SE2, E1, E2>, + V: ExprKindVisitor<'a, SE1, SE2, E1, E2>, { fn vec<'a, T, U, Err, F: FnMut(&'a T) -> Result<U, Err>>( x: &'a [T], @@ -83,7 +83,7 @@ where where SE1: 'a, T: FromIterator<(Label, SE2)>, - V: ExprFVisitor<'a, SE1, SE2, E1, E2>, + V: ExprKindVisitor<'a, SE1, SE2, E1, E2>, { x.into_iter() .map(|(k, x)| Ok((k.clone(), v.visit_subexpr(x)?))) @@ -96,7 +96,7 @@ where where SE1: 'a, T: FromIterator<(Label, Option<SE2>)>, - V: ExprFVisitor<'a, SE1, SE2, E1, E2>, + V: ExprKindVisitor<'a, SE1, SE2, E1, E2>, { x.into_iter() .map(|(k, x)| { @@ -111,7 +111,7 @@ where .collect() } - use crate::syntax::ExprF::*; + use crate::syntax::ExprKind::*; Ok(match input { Var(v) => Var(v.clone()), Lam(l, t, e) => { @@ -172,14 +172,14 @@ where fn visit_mut<'a, V, SE, E>( mut v: V, - input: &'a mut ExprF<SE, E>, + input: &'a mut ExprKind<SE, E>, ) -> Result<(), V::Error> where - V: ExprFMutVisitor<'a, SE, E>, + V: ExprKindMutVisitor<'a, SE, E>, { fn vec<'a, V, SE, E>(v: &mut V, x: &'a mut Vec<SE>) -> Result<(), V::Error> where - V: ExprFMutVisitor<'a, SE, E>, + V: ExprKindMutVisitor<'a, SE, E>, { for x in x { v.visit_subexpr(x)?; @@ -191,7 +191,7 @@ where x: &'a mut Option<SE>, ) -> Result<(), V::Error> where - V: ExprFMutVisitor<'a, SE, E>, + V: ExprKindMutVisitor<'a, SE, E>, { if let Some(x) = x { v.visit_subexpr(x)?; @@ -204,7 +204,7 @@ where ) -> Result<(), V::Error> where SE: 'a, - V: ExprFMutVisitor<'a, SE, E>, + V: ExprKindMutVisitor<'a, SE, E>, { for (_, x) in x { v.visit_subexpr(x)?; @@ -217,7 +217,7 @@ where ) -> Result<(), V::Error> where SE: 'a, - V: ExprFMutVisitor<'a, SE, E>, + V: ExprKindMutVisitor<'a, SE, E>, { for (_, x) in x { opt(&mut v, x)?; @@ -225,7 +225,7 @@ where Ok(()) } - use crate::syntax::ExprF::*; + use crate::syntax::ExprKind::*; match input { Var(_) | Const(_) | Builtin(_) | BoolLit(_) | NaturalLit(_) | IntegerLit(_) | DoubleLit(_) => {} @@ -293,7 +293,7 @@ pub struct TraverseRefWithBindersVisitor<F1, F2> { pub visit_under_binder: F2, } -impl<'a, SE, E, SE2, Err, F1, F2> ExprFVisitor<'a, SE, SE2, E, E> +impl<'a, SE, E, SE2, Err, F1, F2> ExprKindVisitor<'a, SE, SE2, E, E> for TraverseRefWithBindersVisitor<F1, F2> where SE: 'a, @@ -322,7 +322,7 @@ pub struct TraverseRefVisitor<F1> { pub visit_subexpr: F1, } -impl<'a, SE, E, SE2, Err, F1> ExprFVisitor<'a, SE, SE2, E, E> +impl<'a, SE, E, SE2, Err, F1> ExprKindVisitor<'a, SE, SE2, E, E> for TraverseRefVisitor<F1> where SE: 'a, @@ -343,7 +343,8 @@ pub struct TraverseMutVisitor<F1> { pub visit_subexpr: F1, } -impl<'a, SE, E, Err, F1> ExprFMutVisitor<'a, SE, E> for TraverseMutVisitor<F1> +impl<'a, SE, E, Err, F1> ExprKindMutVisitor<'a, SE, E> + for TraverseMutVisitor<F1> where SE: 'a, E: 'a, diff --git a/dhall/src/syntax/binary/decode.rs b/dhall/src/syntax/binary/decode.rs index 46c9921..254ab07 100644 --- a/dhall/src/syntax/binary/decode.rs +++ b/dhall/src/syntax/binary/decode.rs @@ -2,12 +2,13 @@ use itertools::Itertools; use serde_cbor::value::value as cbor; use std::iter::FromIterator; -use crate::semantics::error::DecodeError; +use crate::error::DecodeError; use crate::semantics::phase::DecodedExpr; use crate::syntax; use crate::syntax::{ - Expr, ExprF, FilePath, FilePrefix, Hash, ImportLocation, ImportMode, - Integer, InterpolatedText, Label, Natural, RawExpr, Scheme, Span, URL, V, + Expr, ExprKind, FilePath, FilePrefix, Hash, ImportLocation, ImportMode, + Integer, InterpolatedText, Label, Natural, Scheme, Span, UnspannedExpr, + URL, V, }; pub(crate) fn decode(data: &[u8]) -> Result<DecodedExpr, DecodeError> { @@ -18,17 +19,17 @@ pub(crate) fn decode(data: &[u8]) -> Result<DecodedExpr, DecodeError> { } // Should probably rename this -fn rc<E>(x: RawExpr<E>) -> Expr<E> { +fn rc<E>(x: UnspannedExpr<E>) -> Expr<E> { Expr::new(x, Span::Decoded) } fn cbor_value_to_dhall(data: &cbor::Value) -> Result<DecodedExpr, DecodeError> { use cbor::Value::*; use syntax::{BinOp, Builtin, Const}; - use ExprF::*; + use ExprKind::*; Ok(rc(match data { String(s) => match Builtin::parse(s) { - Some(b) => ExprF::Builtin(b), + Some(b) => ExprKind::Builtin(b), None => match s.as_str() { "True" => BoolLit(true), "False" => BoolLit(false), @@ -123,7 +124,7 @@ fn cbor_value_to_dhall(data: &cbor::Value) -> Result<DecodedExpr, DecodeError> { } [U64(4), t] => { let t = cbor_value_to_dhall(&t)?; - EmptyListLit(rc(App(rc(ExprF::Builtin(Builtin::List)), t))) + EmptyListLit(rc(App(rc(ExprKind::Builtin(Builtin::List)), t))) } [U64(4), Null, rest @ ..] => { let rest = rest @@ -139,14 +140,14 @@ fn cbor_value_to_dhall(data: &cbor::Value) -> Result<DecodedExpr, DecodeError> { // Old-style optional literals [U64(5), t] => { let t = cbor_value_to_dhall(&t)?; - App(rc(ExprF::Builtin(Builtin::OptionalNone)), t) + App(rc(ExprKind::Builtin(Builtin::OptionalNone)), t) } [U64(5), t, x] => { let x = cbor_value_to_dhall(&x)?; let t = cbor_value_to_dhall(&t)?; Annot( rc(SomeLit(x)), - rc(App(rc(ExprF::Builtin(Builtin::Optional)), t)), + rc(App(rc(ExprKind::Builtin(Builtin::Optional)), t)), ) } [U64(6), x, y] => { diff --git a/dhall/src/syntax/binary/encode.rs b/dhall/src/syntax/binary/encode.rs index 8e13efd..25a545c 100644 --- a/dhall/src/syntax/binary/encode.rs +++ b/dhall/src/syntax/binary/encode.rs @@ -1,12 +1,12 @@ use serde_cbor::value::value as cbor; use std::vec; -use crate::semantics::error::EncodeError; +use crate::error::EncodeError; use crate::syntax; use crate::syntax::map::DupTreeMap; use crate::syntax::{ - Expr, ExprF, FilePrefix, Hash, Import, ImportLocation, ImportMode, Label, - Scheme, V, + Expr, ExprKind, FilePrefix, Hash, Import, ImportLocation, ImportMode, + Label, Scheme, V, }; /// Warning: will fail if `expr` contains an `Embed` node. @@ -46,7 +46,7 @@ where use cbor::Value::{String, I64, U64}; use std::iter::once; use syntax::Builtin; - use syntax::ExprF::*; + use syntax::ExprKind::*; use self::Serialize::{RecordMap, UnionMap}; fn expr<E>(x: &Expr<E>) -> self::Serialize<'_, E> { @@ -110,7 +110,9 @@ where SomeLit(x) => ser_seq!(ser; tag(5), null(), expr(x)), EmptyListLit(x) => match x.as_ref() { App(f, a) => match f.as_ref() { - ExprF::Builtin(Builtin::List) => ser_seq!(ser; tag(4), expr(a)), + ExprKind::Builtin(Builtin::List) => { + ser_seq!(ser; tag(4), expr(a)) + } _ => ser_seq!(ser; tag(28), expr(x)), }, _ => ser_seq!(ser; tag(28), expr(x)), @@ -284,7 +286,7 @@ fn collect_nested_applications<'a, E>( ) -> (&'a Expr<E>, Vec<&'a Expr<E>>) { fn go<'a, E>(e: &'a Expr<E>, vec: &mut Vec<&'a Expr<E>>) -> &'a Expr<E> { match e.as_ref() { - ExprF::App(f, a) => { + ExprKind::App(f, a) => { vec.push(a); go(f, vec) } @@ -306,7 +308,7 @@ fn collect_nested_lets<'a, E>( vec: &mut Vec<LetBinding<'a, E>>, ) -> &'a Expr<E> { match e.as_ref() { - ExprF::Let(l, t, v, e) => { + ExprKind::Let(l, t, v, e) => { vec.push((l, t, v)); go(e, vec) } diff --git a/dhall/src/syntax/core/context.rs b/dhall/src/syntax/core/context.rs deleted file mode 100644 index 6844baa..0000000 --- a/dhall/src/syntax/core/context.rs +++ /dev/null @@ -1,80 +0,0 @@ -use std::cmp::Eq; -use std::collections::HashMap; -use std::hash::Hash; - -/// A `(Context a)` associates `Text` labels with values of type `a` -/// -/// The `Context` is used for type-checking when `(a = Expr)` -/// -/// * You create a `Context` using `empty` and `insert` -/// * You transform a `Context` using `fmap` -/// * You consume a `Context` using `lookup` and `toList` -/// -/// The difference between a `Context` and a `Map` is that a `Context` lets you -/// have multiple ordered occurrences of the same key and you can query for the -/// `n`th occurrence of a given key. -/// -#[derive(Debug, Clone)] -pub struct Context<K: Eq + Hash, T>(HashMap<K, Vec<T>>); - -impl<K: Hash + Eq + Clone, T> Context<K, T> { - /// An empty context with no key-value pairs - pub fn new() -> Self { - Context(HashMap::new()) - } - - /// Look up a key by name and index - /// - /// ```c - /// lookup _ _ empty = Nothing - /// lookup k 0 (insert k v c) = Just v - /// lookup k n (insert k v c) = lookup k (n - 1) c -- 1 <= n - /// lookup k n (insert j v c) = lookup k n c -- k /= j - /// ``` - pub fn lookup<'a>(&'a self, k: &K, n: usize) -> Option<&'a T> { - self.0.get(k).and_then(|v| { - if n < v.len() { - v.get(v.len() - 1 - n) - } else { - None - } - }) - } - - pub fn map<U, F: Fn(&K, &T) -> U>(&self, f: F) -> Context<K, U> { - Context( - self.0 - .iter() - .map(|(k, vs)| { - ((*k).clone(), vs.iter().map(|v| f(k, v)).collect()) - }) - .collect(), - ) - } - - pub fn lookup_all<'a>(&'a self, k: &K) -> impl Iterator<Item = &T> { - self.0.get(k).into_iter().flat_map(|v| v.iter()) - } - - pub fn iter(&self) -> impl Iterator<Item = (&K, &T)> { - self.0 - .iter() - .flat_map(|(k, vs)| vs.iter().map(move |v| (k, v))) - } - - pub fn iter_keys(&self) -> impl Iterator<Item = (&K, &Vec<T>)> { - self.0.iter() - } -} - -impl<K: Hash + Eq + Clone, T: Clone> Context<K, T> { - /// Add a key-value pair to the `Context` - pub fn insert(&self, k: K, v: T) -> Self { - let mut ctx = (*self).clone(); - { - let m = ctx.0.entry(k).or_insert_with(Vec::new); - m.push(v); - } - ctx - } -} diff --git a/dhall/src/syntax/mod.rs b/dhall/src/syntax/mod.rs index a82e827..512a026 100644 --- a/dhall/src/syntax/mod.rs +++ b/dhall/src/syntax/mod.rs @@ -5,10 +5,9 @@ clippy::type_complexity )] -mod core; -pub use crate::syntax::core::context; -pub use crate::syntax::core::visitor; -pub use crate::syntax::core::*; +mod ast; +pub use crate::syntax::ast::visitor; +pub use crate::syntax::ast::*; pub use crate::syntax::text::parser::*; pub use crate::syntax::text::printer::*; pub mod binary; diff --git a/dhall/src/syntax/text/parser.rs b/dhall/src/syntax/text/parser.rs index f6b6577..90cb4b1 100644 --- a/dhall/src/syntax/text/parser.rs +++ b/dhall/src/syntax/text/parser.rs @@ -7,13 +7,12 @@ use pest_consume::{match_nodes, Parser}; use crate::semantics::phase::Normalized; use crate::syntax; -use crate::syntax::core; use crate::syntax::map::{DupTreeMap, DupTreeSet}; -use crate::syntax::ExprF::*; +use crate::syntax::ExprKind::*; use crate::syntax::{ - FilePath, FilePrefix, Hash, ImportLocation, ImportMode, InterpolatedText, - InterpolatedTextContents, Label, NaiveDouble, RawExpr, Scheme, Span, URL, - V, + Double, FilePath, FilePrefix, Hash, ImportLocation, ImportMode, Integer, + InterpolatedText, InterpolatedTextContents, Label, NaiveDouble, Natural, + Scheme, Span, UnspannedExpr, URL, V, }; // This file consumes the parse tree generated by pest and turns it into @@ -77,10 +76,14 @@ impl crate::syntax::Builtin { fn input_to_span(input: ParseInput) -> Span { Span::make(input.user_data().clone(), input.as_pair().as_span()) } -fn spanned(input: ParseInput, x: RawExpr<Normalized>) -> Expr { +fn spanned(input: ParseInput, x: UnspannedExpr<Normalized>) -> Expr { Expr::new(x, input_to_span(input)) } -fn spanned_union(span1: Span, span2: Span, x: RawExpr<Normalized>) -> Expr { +fn spanned_union( + span1: Span, + span2: Span, + x: UnspannedExpr<Normalized>, +) -> Expr { Expr::new(x, span1.union(&span2)) } @@ -349,20 +352,20 @@ impl DhallParser { } #[alias(double_literal)] - fn NaN(_input: ParseInput) -> ParseResult<core::Double> { + fn NaN(_input: ParseInput) -> ParseResult<Double> { Ok(std::f64::NAN.into()) } #[alias(double_literal)] - fn minus_infinity_literal(_input: ParseInput) -> ParseResult<core::Double> { + fn minus_infinity_literal(_input: ParseInput) -> ParseResult<Double> { Ok(std::f64::NEG_INFINITY.into()) } #[alias(double_literal)] - fn plus_infinity_literal(_input: ParseInput) -> ParseResult<core::Double> { + fn plus_infinity_literal(_input: ParseInput) -> ParseResult<Double> { Ok(std::f64::INFINITY.into()) } #[alias(double_literal)] - fn numeric_double_literal(input: ParseInput) -> ParseResult<core::Double> { + fn numeric_double_literal(input: ParseInput) -> ParseResult<Double> { let s = input.as_str().trim(); match s.parse::<f64>() { Ok(x) if x.is_infinite() => Err(input.error(format!( @@ -374,7 +377,7 @@ impl DhallParser { } } - fn natural_literal(input: ParseInput) -> ParseResult<core::Natural> { + fn natural_literal(input: ParseInput) -> ParseResult<Natural> { input .as_str() .trim() @@ -382,7 +385,7 @@ impl DhallParser { .map_err(|e| input.error(format!("{}", e))) } - fn integer_literal(input: ParseInput) -> ParseResult<core::Integer> { + fn integer_literal(input: ParseInput) -> ParseResult<Integer> { input .as_str() .trim() diff --git a/dhall/src/syntax/text/printer.rs b/dhall/src/syntax/text/printer.rs index 8df456b..78942ed 100644 --- a/dhall/src/syntax/text/printer.rs +++ b/dhall/src/syntax/text/printer.rs @@ -2,10 +2,137 @@ use crate::syntax::*; use itertools::Itertools; use std::fmt::{self, Display}; +// There is a one-to-one correspondence between the formatter and the grammar. Each phase is +// named after a corresponding grammar group, and the structure of the formatter reflects +// the relationship between the corresponding grammar rules. This leads to the nice property +// of automatically getting all the parentheses and precedences right. +#[derive(Debug, Copy, Clone, Ord, PartialOrd, Eq, PartialEq)] +enum PrintPhase { + Base, + Operator, + BinOp(ast::BinOp), + App, + Import, + Primitive, +} + +// Wraps an Expr with a phase, so that phase selection can be done separate from the actual +// printing. +#[derive(Clone)] +struct PhasedExpr<'a, E>(&'a Expr<E>, PrintPhase); + +impl<'a, E: Display + Clone> PhasedExpr<'a, E> { + fn phase(self, phase: PrintPhase) -> PhasedExpr<'a, E> { + PhasedExpr(self.0, phase) + } +} + +impl<E: Display + Clone> UnspannedExpr<E> { + // Annotate subexpressions with the appropriate phase, defaulting to Base + fn annotate_with_phases<'a>(&'a self) -> ExprKind<PhasedExpr<'a, E>, E> { + use crate::syntax::ExprKind::*; + use PrintPhase::*; + let with_base = self.map_ref(|e| PhasedExpr(e, Base)); + match with_base { + Pi(a, b, c) => { + if &String::from(&a) == "_" { + Pi(a, b.phase(Operator), c) + } else { + Pi(a, b, c) + } + } + Merge(a, b, c) => Merge( + a.phase(PrintPhase::Import), + b.phase(PrintPhase::Import), + c.map(|x| x.phase(PrintPhase::App)), + ), + ToMap(a, b) => ToMap( + a.phase(PrintPhase::Import), + b.map(|x| x.phase(PrintPhase::App)), + ), + Annot(a, b) => Annot(a.phase(Operator), b), + ExprKind::BinOp(op, a, b) => ExprKind::BinOp( + op, + a.phase(PrintPhase::BinOp(op)), + b.phase(PrintPhase::BinOp(op)), + ), + SomeLit(e) => SomeLit(e.phase(PrintPhase::Import)), + ExprKind::App(f, a) => ExprKind::App( + f.phase(PrintPhase::Import), + a.phase(PrintPhase::Import), + ), + Field(a, b) => Field(a.phase(Primitive), b), + Projection(e, ls) => Projection(e.phase(Primitive), ls), + ProjectionByExpr(a, b) => ProjectionByExpr(a.phase(Primitive), b), + e => e, + } + } + + fn fmt_phase( + &self, + f: &mut fmt::Formatter, + phase: PrintPhase, + ) -> Result<(), fmt::Error> { + use crate::syntax::ExprKind::*; + + let needs_paren = match self { + Lam(_, _, _) + | BoolIf(_, _, _) + | Pi(_, _, _) + | Let(_, _, _, _) + | EmptyListLit(_) + | NEListLit(_) + | SomeLit(_) + | Merge(_, _, _) + | ToMap(_, _) + | Annot(_, _) => phase > PrintPhase::Base, + // Precedence is magically handled by the ordering of BinOps. + ExprKind::BinOp(op, _, _) => phase > PrintPhase::BinOp(*op), + ExprKind::App(_, _) => phase > PrintPhase::App, + Field(_, _) | Projection(_, _) | ProjectionByExpr(_, _) => { + phase > PrintPhase::Import + } + _ => false, + }; + + if needs_paren { + f.write_str("(")?; + } + self.annotate_with_phases().fmt(f)?; + if needs_paren { + f.write_str(")")?; + } + + Ok(()) + } +} + +fn fmt_list<T, I, F>( + open: &str, + sep: &str, + close: &str, + it: I, + f: &mut fmt::Formatter, + func: F, +) -> Result<(), fmt::Error> +where + I: IntoIterator<Item = T>, + F: Fn(T, &mut fmt::Formatter) -> Result<(), fmt::Error>, +{ + f.write_str(open)?; + for (i, x) in it.into_iter().enumerate() { + if i > 0 { + f.write_str(sep)?; + } + func(x, f)?; + } + f.write_str(close) +} + /// Generic instance that delegates to subexpressions -impl<SE: Display + Clone, E: Display> Display for ExprF<SE, E> { +impl<SE: Display + Clone, E: Display> Display for ExprKind<SE, E> { fn fmt(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> { - use crate::syntax::ExprF::*; + use crate::syntax::ExprKind::*; match self { Lam(a, b, c) => { write!(f, "λ({} : {}) → {}", a, b, c)?; @@ -53,10 +180,10 @@ impl<SE: Display + Clone, E: Display> Display for ExprF<SE, E> { Assert(a) => { write!(f, "assert : {}", a)?; } - ExprF::BinOp(op, a, b) => { + ExprKind::BinOp(op, a, b) => { write!(f, "{} {} {}", a, op, b)?; } - ExprF::App(a, b) => { + ExprKind::App(a, b) => { write!(f, "{} {}", a, b)?; } Field(a, b) => { @@ -104,147 +231,16 @@ impl<SE: Display + Clone, E: Display> Display for ExprF<SE, E> { } } -// There is a one-to-one correspondence between the formatter and the grammar. Each phase is -// named after a corresponding grammar group, and the structure of the formatter reflects -// the relationship between the corresponding grammar rules. This leads to the nice property -// of automatically getting all the parentheses and precedences right. -#[derive(Debug, Copy, Clone, Ord, PartialOrd, Eq, PartialEq)] -enum PrintPhase { - Base, - Operator, - BinOp(core::BinOp), - App, - Import, - Primitive, -} - -// Wraps an Expr with a phase, so that phase selsction can be done -// separate from the actual printing -#[derive(Clone)] -struct PhasedExpr<'a, A>(&'a Expr<A>, PrintPhase); - -impl<'a, A: Display + Clone> Display for PhasedExpr<'a, A> { - fn fmt(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> { - self.0.as_ref().fmt_phase(f, self.1) - } -} - -impl<'a, A: Display + Clone> PhasedExpr<'a, A> { - fn phase(self, phase: PrintPhase) -> PhasedExpr<'a, A> { - PhasedExpr(self.0, phase) - } -} - -impl<A: Display + Clone> RawExpr<A> { - fn fmt_phase( - &self, - f: &mut fmt::Formatter, - phase: PrintPhase, - ) -> Result<(), fmt::Error> { - use crate::syntax::ExprF::*; - use PrintPhase::*; - - let needs_paren = match self { - Lam(_, _, _) - | BoolIf(_, _, _) - | Pi(_, _, _) - | Let(_, _, _, _) - | EmptyListLit(_) - | NEListLit(_) - | SomeLit(_) - | Merge(_, _, _) - | ToMap(_, _) - | Annot(_, _) - if phase > Base => - { - true - } - // Precedence is magically handled by the ordering of BinOps. - ExprF::BinOp(op, _, _) if phase > PrintPhase::BinOp(*op) => true, - ExprF::App(_, _) if phase > PrintPhase::App => true, - Field(_, _) | Projection(_, _) | ProjectionByExpr(_, _) - if phase > PrintPhase::Import => - { - true - } - _ => false, - }; - - // Annotate subexpressions with the appropriate phase, defaulting to Base - let phased_self = match self.map_ref(|e| PhasedExpr(e, Base)) { - Pi(a, b, c) => { - if &String::from(&a) == "_" { - Pi(a, b.phase(Operator), c) - } else { - Pi(a, b, c) - } - } - Merge(a, b, c) => Merge( - a.phase(PrintPhase::Import), - b.phase(PrintPhase::Import), - c.map(|x| x.phase(PrintPhase::App)), - ), - ToMap(a, b) => ToMap( - a.phase(PrintPhase::Import), - b.map(|x| x.phase(PrintPhase::App)), - ), - Annot(a, b) => Annot(a.phase(Operator), b), - ExprF::BinOp(op, a, b) => ExprF::BinOp( - op, - a.phase(PrintPhase::BinOp(op)), - b.phase(PrintPhase::BinOp(op)), - ), - SomeLit(e) => SomeLit(e.phase(PrintPhase::Import)), - ExprF::App(f, a) => ExprF::App( - f.phase(PrintPhase::Import), - a.phase(PrintPhase::Import), - ), - Field(a, b) => Field(a.phase(Primitive), b), - Projection(e, ls) => Projection(e.phase(Primitive), ls), - ProjectionByExpr(a, b) => ProjectionByExpr(a.phase(Primitive), b), - e => e, - }; - - if needs_paren { - f.write_str("(")?; - } - - // Uses the ExprF<PhasedExpr<_>, _> instance - phased_self.fmt(f)?; - - if needs_paren { - f.write_str(")")?; - } - Ok(()) - } -} - -impl<A: Display + Clone> Display for Expr<A> { +impl<E: Display + Clone> Display for Expr<E> { fn fmt(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> { self.as_ref().fmt_phase(f, PrintPhase::Base) } } -fn fmt_list<T, I, F>( - open: &str, - sep: &str, - close: &str, - it: I, - f: &mut fmt::Formatter, - func: F, -) -> Result<(), fmt::Error> -where - I: IntoIterator<Item = T>, - F: Fn(T, &mut fmt::Formatter) -> Result<(), fmt::Error>, -{ - f.write_str(open)?; - for (i, x) in it.into_iter().enumerate() { - if i > 0 { - f.write_str(sep)?; - } - func(x, f)?; +impl<'a, E: Display + Clone> Display for PhasedExpr<'a, E> { + fn fmt(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> { + self.0.as_ref().fmt_phase(f, self.1) } - f.write_str(close) } impl<SubExpr: Display> Display for InterpolatedText<SubExpr> { @@ -361,6 +357,7 @@ impl Display for Hash { } } } + impl<SubExpr: Display> Display for Import<SubExpr> { fn fmt(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> { use FilePrefix::*; diff --git a/dhall/src/tests.rs b/dhall/src/tests.rs index 9e5c744..d73c2d4 100644 --- a/dhall/src/tests.rs +++ b/dhall/src/tests.rs @@ -47,7 +47,7 @@ use std::fs::File; use std::io::{Read, Write}; use std::path::PathBuf; -use crate::semantics::error::{Error, Result}; +use crate::error::{Error, Result}; use crate::semantics::phase::Parsed; #[allow(dead_code)] |