summaryrefslogtreecommitdiff
path: root/dhall/src/semantics
diff options
context:
space:
mode:
Diffstat (limited to 'dhall/src/semantics')
-rw-r--r--dhall/src/semantics/core/context.rs145
-rw-r--r--dhall/src/semantics/core/mod.rs4
-rw-r--r--dhall/src/semantics/core/value.rs338
-rw-r--r--dhall/src/semantics/core/valuef.rs323
-rw-r--r--dhall/src/semantics/core/var.rs295
-rw-r--r--dhall/src/semantics/error/mod.rs179
-rw-r--r--dhall/src/semantics/mod.rs3
-rw-r--r--dhall/src/semantics/phase/binary.rs748
-rw-r--r--dhall/src/semantics/phase/mod.rs254
-rw-r--r--dhall/src/semantics/phase/normalize.rs794
-rw-r--r--dhall/src/semantics/phase/parse.rs37
-rw-r--r--dhall/src/semantics/phase/resolve.rs180
-rw-r--r--dhall/src/semantics/phase/typecheck.rs815
13 files changed, 4115 insertions, 0 deletions
diff --git a/dhall/src/semantics/core/context.rs b/dhall/src/semantics/core/context.rs
new file mode 100644
index 0000000..00e1493
--- /dev/null
+++ b/dhall/src/semantics/core/context.rs
@@ -0,0 +1,145 @@
+use std::collections::HashMap;
+use std::rc::Rc;
+
+use crate::syntax::{Label, V};
+
+use crate::core::value::Value;
+use crate::core::valuef::ValueF;
+use crate::core::var::{AlphaVar, Shift, Subst};
+use crate::error::TypeError;
+
+#[derive(Debug, Clone)]
+enum CtxItem {
+ Kept(AlphaVar, Value),
+ Replaced(Value),
+}
+
+#[derive(Debug, Clone)]
+pub(crate) struct TypecheckContext(Rc<Vec<(Label, CtxItem)>>);
+
+impl TypecheckContext {
+ pub fn new() -> Self {
+ TypecheckContext(Rc::new(Vec::new()))
+ }
+ pub fn insert_type(&self, x: &Label, t: Value) -> Self {
+ let mut vec = self.0.as_ref().clone();
+ vec.push((x.clone(), CtxItem::Kept(x.into(), t.under_binder(x))));
+ TypecheckContext(Rc::new(vec))
+ }
+ pub fn insert_value(&self, x: &Label, e: Value) -> Result<Self, TypeError> {
+ let mut vec = self.0.as_ref().clone();
+ vec.push((x.clone(), CtxItem::Replaced(e)));
+ Ok(TypecheckContext(Rc::new(vec)))
+ }
+ pub fn lookup(&self, var: &V<Label>) -> Option<Value> {
+ let mut var = var.clone();
+ let mut shift_map: HashMap<Label, _> = HashMap::new();
+ for (l, i) in self.0.iter().rev() {
+ match var.over_binder(l) {
+ None => {
+ 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)
+ }
+ CtxItem::Replaced(v) => v,
+ });
+ }
+ Some(newvar) => var = newvar,
+ };
+ if let CtxItem::Kept(_, _) = i {
+ *shift_map.entry(l.clone()).or_insert(0) += 1;
+ }
+ }
+ // Unbound variable
+ None
+ }
+ /// Given a var that makes sense in the current context, map the given function in such a way
+ /// that the passed variable always makes sense in the context of the passed item.
+ /// Once we pass the variable definition, the variable doesn't make sense anymore so we just
+ /// copy the remaining items.
+ fn do_with_var<E>(
+ &self,
+ var: &AlphaVar,
+ mut f: impl FnMut(&AlphaVar, &CtxItem) -> Result<CtxItem, E>,
+ ) -> Result<Self, E> {
+ let mut vec = Vec::new();
+ vec.reserve(self.0.len());
+ let mut var = var.clone();
+ let mut iter = self.0.iter().rev();
+ for (l, i) in iter.by_ref() {
+ vec.push((l.clone(), f(&var, i)?));
+ if let CtxItem::Kept(_, _) = i {
+ match var.over_binder(l) {
+ None => break,
+ Some(newvar) => var = newvar,
+ };
+ }
+ }
+ for (l, i) in iter {
+ vec.push((l.clone(), (*i).clone()));
+ }
+ vec.reverse();
+ Ok(TypecheckContext(Rc::new(vec)))
+ }
+ fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> {
+ if delta < 0 {
+ Some(self.do_with_var(var, |var, i| Ok(i.shift(delta, &var)?))?)
+ } else {
+ Some(TypecheckContext(Rc::new(
+ self.0
+ .iter()
+ .map(|(l, i)| Ok((l.clone(), i.shift(delta, &var)?)))
+ .collect::<Result<_, _>>()?,
+ )))
+ }
+ }
+ fn subst_shift(&self, var: &AlphaVar, val: &Value) -> Self {
+ self.do_with_var(var, |var, i| Ok::<_, !>(i.subst_shift(&var, val)))
+ .unwrap()
+ }
+}
+
+impl Shift for CtxItem {
+ fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> {
+ Some(match self {
+ CtxItem::Kept(v, t) => {
+ CtxItem::Kept(v.shift(delta, var)?, t.shift(delta, var)?)
+ }
+ CtxItem::Replaced(e) => CtxItem::Replaced(e.shift(delta, var)?),
+ })
+ }
+}
+
+impl Shift for TypecheckContext {
+ fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> {
+ self.shift(delta, var)
+ }
+}
+
+impl Subst<Value> for CtxItem {
+ fn subst_shift(&self, var: &AlphaVar, val: &Value) -> Self {
+ match self {
+ CtxItem::Replaced(e) => CtxItem::Replaced(e.subst_shift(var, val)),
+ CtxItem::Kept(v, t) => match v.shift(-1, var) {
+ None => CtxItem::Replaced(val.clone()),
+ Some(newvar) => CtxItem::Kept(newvar, t.subst_shift(var, val)),
+ },
+ }
+ }
+}
+
+impl Subst<Value> for TypecheckContext {
+ fn subst_shift(&self, var: &AlphaVar, val: &Value) -> Self {
+ self.subst_shift(var, val)
+ }
+}
+
+/// Don't count contexts when comparing stuff.
+/// This is dirty but needed.
+impl PartialEq for TypecheckContext {
+ fn eq(&self, _: &Self) -> bool {
+ true
+ }
+}
+impl Eq for TypecheckContext {}
diff --git a/dhall/src/semantics/core/mod.rs b/dhall/src/semantics/core/mod.rs
new file mode 100644
index 0000000..08213f7
--- /dev/null
+++ b/dhall/src/semantics/core/mod.rs
@@ -0,0 +1,4 @@
+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
new file mode 100644
index 0000000..bd7a9b9
--- /dev/null
+++ b/dhall/src/semantics/core/value.rs
@@ -0,0 +1,338 @@
+use std::cell::{Ref, RefCell, RefMut};
+use std::rc::Rc;
+
+use crate::syntax::{Builtin, Const, Span};
+
+use crate::core::context::TypecheckContext;
+use crate::core::valuef::ValueF;
+use crate::core::var::{AlphaVar, Shift, Subst};
+use crate::error::{TypeError, TypeMessage};
+use crate::phase::normalize::{apply_any, normalize_whnf};
+use crate::phase::typecheck::{builtin_to_value, const_to_value};
+use crate::phase::{NormalizedExpr, Typed};
+
+#[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};
+
+/// 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,
+ /// 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,
+}
+
+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 => {}
+ }
+ }
+
+ fn get_type(&self) -> Result<&Value, TypeError> {
+ match &self.ty {
+ Some(t) => Ok(t),
+ None => {
+ Err(TypeError::new(&TypecheckContext::new(), TypeMessage::Sort))
+ }
+ }
+ }
+}
+
+impl Value {
+ fn new(value: ValueF, form: Form, ty: Value, span: Span) -> Value {
+ ValueInternal {
+ form,
+ value,
+ ty: Some(ty),
+ span,
+ }
+ .into_value()
+ }
+ pub(crate) fn const_sort() -> Value {
+ ValueInternal {
+ form: NF,
+ value: ValueF::Const(Const::Sort),
+ ty: None,
+ span: Span::Artificial,
+ }
+ .into_value()
+ }
+ pub(crate) fn from_valuef_and_type(v: ValueF, t: Value) -> Value {
+ Value::new(v, Unevaled, t, Span::Artificial)
+ }
+ pub(crate) fn from_valuef_and_type_and_span(
+ v: ValueF,
+ t: Value,
+ span: Span,
+ ) -> Value {
+ Value::new(v, Unevaled, t, span)
+ }
+ pub(crate) fn from_valuef_and_type_whnf(v: ValueF, t: Value) -> Value {
+ Value::new(v, WHNF, t, Span::Artificial)
+ }
+ pub(crate) fn from_const(c: Const) -> Self {
+ const_to_value(c)
+ }
+ pub(crate) fn from_builtin(b: Builtin) -> Self {
+ builtin_to_value(b)
+ }
+ pub(crate) fn with_span(self, span: Span) -> Self {
+ self.as_internal_mut().span = span;
+ self
+ }
+
+ pub(crate) fn as_const(&self) -> Option<Const> {
+ match &*self.as_whnf() {
+ ValueF::Const(c) => Some(*c),
+ _ => None,
+ }
+ }
+ pub(crate) fn span(&self) -> Span {
+ self.as_internal().span.clone()
+ }
+
+ fn as_internal(&self) -> Ref<ValueInternal> {
+ self.0.borrow()
+ }
+ 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
+ /// unevaled PartialExpr. You probably want to use `as_whnf`.
+ fn as_valuef(&self) -> Ref<ValueF> {
+ Ref::map(self.as_internal(), ValueInternal::as_valuef)
+ }
+ /// 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> {
+ self.normalize_whnf();
+ self.as_valuef()
+ }
+
+ 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 {
+ 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 {
+ self.check_type(ty);
+ self.to_whnf_ignore_type()
+ }
+ pub(crate) fn into_typed(self) -> Typed {
+ Typed::from_value(self)
+ }
+
+ /// Mutates the contents. If no one else shares this, this avoids a RefCell lock.
+ fn mutate_internal(&mut self, f: impl FnOnce(&mut ValueInternal)) {
+ match Rc::get_mut(&mut self.0) {
+ // Mutate directly if sole owner
+ Some(refcell) => f(RefCell::get_mut(refcell)),
+ // Otherwise mutate through the refcell
+ None => f(&mut self.as_internal_mut()),
+ }
+ }
+ /// Normalizes contents to normal form; faster than `normalize_nf` if
+ /// no one else shares this.
+ pub(crate) fn normalize_mut(&mut self) {
+ self.mutate_internal(|vint| vint.normalize_nf())
+ }
+
+ pub(crate) fn normalize_whnf(&self) {
+ let borrow = self.as_internal();
+ match borrow.form {
+ Unevaled => {
+ drop(borrow);
+ self.as_internal_mut().normalize_whnf();
+ }
+ // Already at least in WHNF
+ WHNF | NF => {}
+ }
+ }
+
+ pub(crate) fn app(&self, v: Value) -> Value {
+ let body_t = match &*self.get_type_not_sort().as_whnf() {
+ ValueF::Pi(x, t, e) => {
+ v.check_type(t);
+ e.subst_shift(&x.into(), &v)
+ }
+ _ => unreachable!("Internal type error"),
+ };
+ Value::from_valuef_and_type_whnf(
+ apply_any(self.clone(), v, &body_t),
+ body_t,
+ )
+ }
+
+ /// In debug mode, panic if the provided type doesn't match the value's type.
+ /// Otherwise does nothing.
+ pub(crate) fn check_type(&self, ty: &Value) {
+ debug_assert_eq!(
+ Some(ty),
+ self.get_type().ok().as_ref(),
+ "Internal type error"
+ );
+ }
+ pub(crate) fn get_type(&self) -> Result<Value, TypeError> {
+ Ok(self.as_internal().get_type()?.clone())
+ }
+ /// When we know the value isn't `Sort`, this gets the type directly
+ pub(crate) fn get_type_not_sort(&self) -> Value {
+ self.get_type()
+ .expect("Internal type error: value is `Sort` but shouldn't be")
+ }
+}
+
+impl Shift for Value {
+ fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> {
+ Some(Value(self.0.shift(delta, var)?))
+ }
+}
+
+impl Shift for ValueInternal {
+ fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> {
+ Some(ValueInternal {
+ form: self.form,
+ value: self.value.shift(delta, var)?,
+ ty: self.ty.shift(delta, var)?,
+ span: self.span.clone(),
+ })
+ }
+}
+
+impl Subst<Value> for Value {
+ fn subst_shift(&self, var: &AlphaVar, val: &Value) -> Self {
+ match &*self.as_valuef() {
+ // 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 => {
+ if let Ok(self_ty) = self.get_type() {
+ val.check_type(&self_ty.subst_shift(var, val));
+ }
+ val.clone()
+ }
+ _ => Value(self.0.subst_shift(var, val)),
+ }
+ }
+}
+
+impl Subst<Value> for ValueInternal {
+ fn subst_shift(&self, var: &AlphaVar, val: &Value) -> Self {
+ ValueInternal {
+ // The resulting value may not stay in wnhf after substitution
+ form: Unevaled,
+ value: self.value.subst_shift(var, val),
+ ty: self.ty.subst_shift(var, val),
+ span: self.span.clone(),
+ }
+ }
+}
+
+// TODO: use Rc comparison to shortcut on identical pointers
+impl std::cmp::PartialEq for Value {
+ fn eq(&self, other: &Self) -> bool {
+ *self.as_whnf() == *other.as_whnf()
+ }
+}
+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 {
+ write!(fmt, "{:?}", c)
+ } else {
+ let mut x = fmt.debug_struct(&format!("Value@{:?}", &vint.form));
+ x.field("value", &vint.value);
+ if let Some(ty) = vint.ty.as_ref() {
+ x.field("type", &ty);
+ } else {
+ x.field("type", &None::<()>);
+ }
+ x.finish()
+ }
+ }
+}
diff --git a/dhall/src/semantics/core/valuef.rs b/dhall/src/semantics/core/valuef.rs
new file mode 100644
index 0000000..e9ac391
--- /dev/null
+++ b/dhall/src/semantics/core/valuef.rs
@@ -0,0 +1,323 @@
+use std::collections::HashMap;
+
+use crate::syntax::{
+ Builtin, Const, ExprF, Integer, InterpolatedTextContents, Label,
+ NaiveDouble, Natural,
+};
+
+use crate::core::value::{ToExprOptions, Value};
+use crate::core::var::{AlphaLabel, AlphaVar, Shift, Subst};
+use crate::phase::typecheck::rc;
+use crate::phase::{Normalized, NormalizedExpr};
+
+/// 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(
+ crate::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
new file mode 100644
index 0000000..f9d3478
--- /dev/null
+++ b/dhall/src/semantics/core/var.rs
@@ -0,0 +1,295 @@
+use std::collections::HashMap;
+
+use crate::syntax::{Label, V};
+
+/// Stores a pair of variables: a normal one and one
+/// that corresponds to the alpha-normalized version of the first one.
+/// Equality is up to alpha-equivalence (compares on the second one only).
+#[derive(Clone, Eq)]
+pub struct AlphaVar {
+ normal: V<Label>,
+ alpha: V<()>,
+}
+
+// Exactly like a Label, but equality returns always true.
+// This is so that ValueF equality is exactly alpha-equivalence.
+#[derive(Clone, Eq)]
+pub struct AlphaLabel(Label);
+
+pub(crate) trait Shift: Sized {
+ // Shift an expression to move it around binders without changing the meaning of its free
+ // variables. Shift by 1 to move an expression under a binder. Shift by -1 to extract an
+ // expression from under a binder, if the expression does not refer to that bound variable.
+ // Returns None if delta was negative and the variable was free in the expression.
+ fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self>;
+
+ fn over_binder<T>(&self, x: T) -> Option<Self>
+ where
+ T: Into<AlphaVar>,
+ {
+ self.shift(-1, &x.into())
+ }
+
+ fn under_binder<T>(&self, x: T) -> Self
+ where
+ T: Into<AlphaVar>,
+ {
+ // Can't fail since delta is positive
+ self.shift(1, &x.into()).unwrap()
+ }
+
+ fn under_multiple_binders(&self, shift_map: &HashMap<Label, usize>) -> Self
+ where
+ Self: Clone,
+ {
+ let mut v = self.clone();
+ for (x, n) in shift_map {
+ v = v.shift(*n as isize, &x.into()).unwrap();
+ }
+ v
+ }
+}
+
+pub(crate) trait Subst<S> {
+ fn subst_shift(&self, var: &AlphaVar, val: &S) -> Self;
+}
+
+impl AlphaVar {
+ pub(crate) fn to_var(&self, alpha: bool) -> V<Label> {
+ if alpha {
+ V("_".into(), self.alpha.1)
+ } else {
+ self.normal.clone()
+ }
+ }
+ pub(crate) fn from_var_and_alpha(normal: V<Label>, alpha: usize) -> Self {
+ AlphaVar {
+ normal,
+ alpha: V((), alpha),
+ }
+ }
+}
+
+impl AlphaLabel {
+ pub(crate) fn to_label_maybe_alpha(&self, alpha: bool) -> Label {
+ if alpha {
+ "_".into()
+ } else {
+ self.to_label()
+ }
+ }
+ pub(crate) fn to_label(&self) -> Label {
+ self.clone().into()
+ }
+}
+
+impl Shift for AlphaVar {
+ fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> {
+ Some(AlphaVar {
+ normal: self.normal.shift(delta, &var.normal)?,
+ alpha: self.alpha.shift(delta, &var.alpha)?,
+ })
+ }
+}
+
+/// Equality up to alpha-equivalence
+impl std::cmp::PartialEq for AlphaVar {
+ fn eq(&self, other: &Self) -> bool {
+ self.alpha == other.alpha
+ }
+}
+impl std::cmp::PartialEq for AlphaLabel {
+ fn eq(&self, _other: &Self) -> bool {
+ true
+ }
+}
+
+impl std::fmt::Debug for AlphaVar {
+ fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
+ write!(f, "AlphaVar({}, {})", self.normal, self.alpha.1)
+ }
+}
+
+impl std::fmt::Debug for AlphaLabel {
+ fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
+ write!(f, "AlphaLabel({})", &self.0)
+ }
+}
+
+impl From<Label> for AlphaVar {
+ fn from(x: Label) -> AlphaVar {
+ AlphaVar {
+ normal: V(x, 0),
+ alpha: V((), 0),
+ }
+ }
+}
+impl<'a> From<&'a Label> for AlphaVar {
+ fn from(x: &'a Label) -> AlphaVar {
+ x.clone().into()
+ }
+}
+impl From<AlphaLabel> for AlphaVar {
+ fn from(x: AlphaLabel) -> AlphaVar {
+ let l: Label = x.into();
+ l.into()
+ }
+}
+impl<'a> From<&'a AlphaLabel> for AlphaVar {
+ fn from(x: &'a AlphaLabel) -> AlphaVar {
+ x.clone().into()
+ }
+}
+
+impl From<Label> for AlphaLabel {
+ fn from(x: Label) -> AlphaLabel {
+ AlphaLabel(x)
+ }
+}
+impl From<AlphaLabel> for Label {
+ fn from(x: AlphaLabel) -> Label {
+ x.0
+ }
+}
+impl Shift for () {
+ fn shift(&self, _delta: isize, _var: &AlphaVar) -> Option<Self> {
+ Some(())
+ }
+}
+
+impl<A: Shift, B: Shift> Shift for (A, B) {
+ fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> {
+ Some((self.0.shift(delta, var)?, self.1.shift(delta, var)?))
+ }
+}
+
+impl<T: Shift> Shift for Option<T> {
+ fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> {
+ Some(match self {
+ None => None,
+ Some(x) => Some(x.shift(delta, var)?),
+ })
+ }
+}
+
+impl<T: Shift> Shift for Box<T> {
+ fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> {
+ Some(Box::new(self.as_ref().shift(delta, var)?))
+ }
+}
+
+impl<T: Shift> Shift for std::rc::Rc<T> {
+ fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> {
+ Some(std::rc::Rc::new(self.as_ref().shift(delta, var)?))
+ }
+}
+
+impl<T: Shift> Shift for std::cell::RefCell<T> {
+ fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> {
+ Some(std::cell::RefCell::new(self.borrow().shift(delta, var)?))
+ }
+}
+
+impl<T: Shift, E: Clone> Shift for crate::syntax::ExprF<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)?),
+ |x, v| Ok(v.shift(delta, &var.under_binder(x))?),
+ )?)
+ }
+}
+
+impl<T: Shift> Shift for Vec<T> {
+ fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> {
+ Some(
+ self.iter()
+ .map(|v| Ok(v.shift(delta, var)?))
+ .collect::<Result<_, _>>()?,
+ )
+ }
+}
+
+impl<K, T: Shift> Shift for HashMap<K, T>
+where
+ K: Clone + std::hash::Hash + Eq,
+{
+ fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> {
+ Some(
+ self.iter()
+ .map(|(k, v)| Ok((k.clone(), v.shift(delta, var)?)))
+ .collect::<Result<_, _>>()?,
+ )
+ }
+}
+
+impl<T: Shift> Shift for crate::syntax::InterpolatedTextContents<T> {
+ fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> {
+ Some(self.traverse_ref(|x| Ok(x.shift(delta, var)?))?)
+ }
+}
+
+impl<S> Subst<S> for () {
+ fn subst_shift(&self, _var: &AlphaVar, _val: &S) -> Self {}
+}
+
+impl<S, A: Subst<S>, B: Subst<S>> Subst<S> for (A, B) {
+ fn subst_shift(&self, var: &AlphaVar, val: &S) -> Self {
+ (self.0.subst_shift(var, val), self.1.subst_shift(var, val))
+ }
+}
+
+impl<S, T: Subst<S>> Subst<S> for Option<T> {
+ fn subst_shift(&self, var: &AlphaVar, val: &S) -> Self {
+ self.as_ref().map(|x| x.subst_shift(var, val))
+ }
+}
+
+impl<S, T: Subst<S>> Subst<S> for Box<T> {
+ fn subst_shift(&self, var: &AlphaVar, val: &S) -> Self {
+ Box::new(self.as_ref().subst_shift(var, val))
+ }
+}
+
+impl<S, T: Subst<S>> Subst<S> for std::rc::Rc<T> {
+ fn subst_shift(&self, var: &AlphaVar, val: &S) -> Self {
+ std::rc::Rc::new(self.as_ref().subst_shift(var, val))
+ }
+}
+
+impl<S, T: Subst<S>> Subst<S> for std::cell::RefCell<T> {
+ fn subst_shift(&self, var: &AlphaVar, val: &S) -> Self {
+ std::cell::RefCell::new(self.borrow().subst_shift(var, val))
+ }
+}
+
+impl<S: Shift, T: Subst<S>, E: Clone> Subst<S> for crate::syntax::ExprF<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),
+ |x, v| v.subst_shift(&var.under_binder(x), &val.under_binder(x)),
+ )
+ }
+}
+
+impl<S, T: Subst<S>> Subst<S> for Vec<T> {
+ fn subst_shift(&self, var: &AlphaVar, val: &S) -> Self {
+ self.iter().map(|v| v.subst_shift(var, val)).collect()
+ }
+}
+
+impl<S, T: Subst<S>> Subst<S> for crate::syntax::InterpolatedTextContents<T> {
+ fn subst_shift(&self, var: &AlphaVar, val: &S) -> Self {
+ self.map_ref(|x| x.subst_shift(var, val))
+ }
+}
+
+impl<S, K, T: Subst<S>> Subst<S> for HashMap<K, T>
+where
+ K: Clone + std::hash::Hash + Eq,
+{
+ fn subst_shift(&self, var: &AlphaVar, val: &S) -> Self {
+ self.iter()
+ .map(|(k, v)| (k.clone(), v.subst_shift(var, val)))
+ .collect()
+ }
+}
diff --git a/dhall/src/semantics/error/mod.rs b/dhall/src/semantics/error/mod.rs
new file mode 100644
index 0000000..1d58e6f
--- /dev/null
+++ b/dhall/src/semantics/error/mod.rs
@@ -0,0 +1,179 @@
+use std::io::Error as IOError;
+
+use crate::syntax::{BinOp, Import, Label, ParseError, Span};
+
+use crate::core::context::TypecheckContext;
+use crate::core::value::Value;
+use crate::phase::resolve::ImportStack;
+use crate::phase::NormalizedExpr;
+
+pub type Result<T> = std::result::Result<T, Error>;
+
+#[derive(Debug)]
+#[non_exhaustive]
+pub enum Error {
+ IO(IOError),
+ Parse(ParseError),
+ Decode(DecodeError),
+ Encode(EncodeError),
+ Resolve(ImportError),
+ Typecheck(TypeError),
+}
+
+#[derive(Debug)]
+pub enum ImportError {
+ Recursive(Import<NormalizedExpr>, Box<Error>),
+ UnexpectedImport(Import<NormalizedExpr>),
+ ImportCycle(ImportStack, Import<NormalizedExpr>),
+}
+
+#[derive(Debug)]
+pub enum DecodeError {
+ CBORError(serde_cbor::error::Error),
+ WrongFormatError(String),
+}
+
+#[derive(Debug)]
+pub enum EncodeError {
+ CBORError(serde_cbor::error::Error),
+}
+
+/// A structured type error that includes context
+#[derive(Debug)]
+pub struct TypeError {
+ message: TypeMessage,
+ context: TypecheckContext,
+}
+
+/// The specific type error
+#[derive(Debug)]
+pub(crate) enum TypeMessage {
+ UnboundVariable(Span),
+ InvalidInputType(Value),
+ InvalidOutputType(Value),
+ NotAFunction(Value),
+ TypeMismatch(Value, Value, Value),
+ AnnotMismatch(Value, Value),
+ InvalidListElement(usize, Value, Value),
+ InvalidListType(Value),
+ InvalidOptionalType(Value),
+ InvalidPredicate(Value),
+ IfBranchMismatch(Value, Value),
+ IfBranchMustBeTerm(bool, Value),
+ InvalidFieldType(Label, Value),
+ NotARecord(Label, Value),
+ MustCombineRecord(Value),
+ MissingRecordField(Label, Value),
+ MissingUnionField(Label, Value),
+ BinOpTypeMismatch(BinOp, Value),
+ InvalidTextInterpolation(Value),
+ Merge1ArgMustBeRecord(Value),
+ Merge2ArgMustBeUnion(Value),
+ MergeEmptyNeedsAnnotation,
+ MergeHandlerMissingVariant(Label),
+ MergeVariantMissingHandler(Label),
+ MergeAnnotMismatch,
+ MergeHandlerTypeMismatch,
+ MergeHandlerReturnTypeMustNotBeDependent,
+ ProjectionMustBeRecord,
+ ProjectionMissingEntry,
+ Sort,
+ RecordTypeDuplicateField,
+ RecordTypeMergeRequiresRecordType(Value),
+ UnionTypeDuplicateField,
+ EquivalenceArgumentMustBeTerm(bool, Value),
+ EquivalenceTypeMismatch(Value, Value),
+ AssertMismatch(Value, Value),
+ AssertMustTakeEquivalence,
+}
+
+impl TypeError {
+ pub(crate) fn new(
+ context: &TypecheckContext,
+ message: TypeMessage,
+ ) -> Self {
+ TypeError {
+ context: context.clone(),
+ message,
+ }
+ }
+}
+
+impl std::fmt::Display for TypeError {
+ fn fmt(&self, f: &mut std::fmt::Formatter) -> std::fmt::Result {
+ use TypeMessage::*;
+ let msg = match &self.message {
+ UnboundVariable(span) => span.error("Type error: Unbound variable"),
+ InvalidInputType(v) => {
+ v.span().error("Type error: Invalid function input")
+ }
+ InvalidOutputType(v) => {
+ v.span().error("Type error: Invalid function output")
+ }
+ NotAFunction(v) => v.span().error("Type error: Not a function"),
+ TypeMismatch(x, y, z) => {
+ x.span()
+ .error("Type error: Wrong type of function argument")
+ + "\n"
+ + &z.span().error(format!(
+ "This argument has type {:?}",
+ z.get_type().unwrap()
+ ))
+ + "\n"
+ + &y.span().error(format!(
+ "But the function expected an argument of type {:?}",
+ y
+ ))
+ }
+ _ => "Type error: Unhandled error".to_string(),
+ };
+ write!(f, "{}", msg)
+ }
+}
+
+impl std::error::Error for TypeError {}
+
+impl std::fmt::Display for Error {
+ fn fmt(&self, f: &mut std::fmt::Formatter) -> std::fmt::Result {
+ match self {
+ Error::IO(err) => write!(f, "{}", err),
+ Error::Parse(err) => write!(f, "{}", err),
+ Error::Decode(err) => write!(f, "{:?}", err),
+ Error::Encode(err) => write!(f, "{:?}", err),
+ Error::Resolve(err) => write!(f, "{:?}", err),
+ Error::Typecheck(err) => write!(f, "{}", err),
+ }
+ }
+}
+
+impl std::error::Error for Error {}
+impl From<IOError> for Error {
+ fn from(err: IOError) -> Error {
+ Error::IO(err)
+ }
+}
+impl From<ParseError> for Error {
+ fn from(err: ParseError) -> Error {
+ Error::Parse(err)
+ }
+}
+impl From<DecodeError> for Error {
+ fn from(err: DecodeError) -> Error {
+ Error::Decode(err)
+ }
+}
+impl From<EncodeError> for Error {
+ fn from(err: EncodeError) -> Error {
+ Error::Encode(err)
+ }
+}
+impl From<ImportError> for Error {
+ fn from(err: ImportError) -> Error {
+ Error::Resolve(err)
+ }
+}
+impl From<TypeError> for Error {
+ fn from(err: TypeError) -> Error {
+ Error::Typecheck(err)
+ }
+}
diff --git a/dhall/src/semantics/mod.rs b/dhall/src/semantics/mod.rs
new file mode 100644
index 0000000..9d2e462
--- /dev/null
+++ b/dhall/src/semantics/mod.rs
@@ -0,0 +1,3 @@
+pub mod core;
+pub mod error;
+pub mod phase;
diff --git a/dhall/src/semantics/phase/binary.rs b/dhall/src/semantics/phase/binary.rs
new file mode 100644
index 0000000..b1e7638
--- /dev/null
+++ b/dhall/src/semantics/phase/binary.rs
@@ -0,0 +1,748 @@
+use itertools::Itertools;
+use serde_cbor::value::value as cbor;
+use std::iter::FromIterator;
+use std::vec;
+
+use crate::syntax::map::DupTreeMap;
+use crate::syntax::{
+ Expr, ExprF, FilePath, FilePrefix, Hash, Import, ImportLocation,
+ ImportMode, Integer, InterpolatedText, Label, Natural, RawExpr, Scheme,
+ Span, URL, V,
+};
+
+use crate::error::{DecodeError, EncodeError};
+use crate::phase::DecodedExpr;
+
+pub(crate) fn decode(data: &[u8]) -> Result<DecodedExpr, DecodeError> {
+ match serde_cbor::de::from_slice(data) {
+ Ok(v) => cbor_value_to_dhall(&v),
+ Err(e) => Err(DecodeError::CBORError(e)),
+ }
+}
+
+pub(crate) fn encode<E>(expr: &Expr<E>) -> Result<Vec<u8>, EncodeError> {
+ serde_cbor::ser::to_vec(&Serialize::Expr(expr))
+ .map_err(|e| EncodeError::CBORError(e))
+}
+
+// Should probably rename this
+pub fn rc<E>(x: RawExpr<E>) -> Expr<E> {
+ Expr::new(x, Span::Decoded)
+}
+
+fn cbor_value_to_dhall(data: &cbor::Value) -> Result<DecodedExpr, DecodeError> {
+ use cbor::Value::*;
+ use crate::syntax::{BinOp, Builtin, Const};
+ use ExprF::*;
+ Ok(rc(match data {
+ String(s) => match Builtin::parse(s) {
+ Some(b) => ExprF::Builtin(b),
+ None => match s.as_str() {
+ "True" => BoolLit(true),
+ "False" => BoolLit(false),
+ "Type" => Const(Const::Type),
+ "Kind" => Const(Const::Kind),
+ "Sort" => Const(Const::Sort),
+ _ => Err(DecodeError::WrongFormatError("builtin".to_owned()))?,
+ },
+ },
+ U64(n) => Var(V(Label::from("_"), *n as usize)),
+ F64(x) => DoubleLit((*x).into()),
+ Bool(b) => BoolLit(*b),
+ Array(vec) => match vec.as_slice() {
+ [String(l), U64(n)] => {
+ if l.as_str() == "_" {
+ Err(DecodeError::WrongFormatError(
+ "`_` variable was encoded incorrectly".to_owned(),
+ ))?
+ }
+ let l = Label::from(l.as_str());
+ Var(V(l, *n as usize))
+ }
+ [U64(0), f, args @ ..] => {
+ if args.is_empty() {
+ Err(DecodeError::WrongFormatError(
+ "Function application must have at least one argument"
+ .to_owned(),
+ ))?
+ }
+ let mut f = cbor_value_to_dhall(&f)?;
+ for a in args {
+ let a = cbor_value_to_dhall(&a)?;
+ f = rc(App(f, a))
+ }
+ return Ok(f);
+ }
+ [U64(1), x, y] => {
+ let x = cbor_value_to_dhall(&x)?;
+ let y = cbor_value_to_dhall(&y)?;
+ Lam(Label::from("_"), x, y)
+ }
+ [U64(1), String(l), x, y] => {
+ if l.as_str() == "_" {
+ Err(DecodeError::WrongFormatError(
+ "`_` variable was encoded incorrectly".to_owned(),
+ ))?
+ }
+ let x = cbor_value_to_dhall(&x)?;
+ let y = cbor_value_to_dhall(&y)?;
+ let l = Label::from(l.as_str());
+ Lam(l, x, y)
+ }
+ [U64(2), x, y] => {
+ let x = cbor_value_to_dhall(&x)?;
+ let y = cbor_value_to_dhall(&y)?;
+ Pi(Label::from("_"), x, y)
+ }
+ [U64(2), String(l), x, y] => {
+ if l.as_str() == "_" {
+ Err(DecodeError::WrongFormatError(
+ "`_` variable was encoded incorrectly".to_owned(),
+ ))?
+ }
+ let x = cbor_value_to_dhall(&x)?;
+ let y = cbor_value_to_dhall(&y)?;
+ let l = Label::from(l.as_str());
+ Pi(l, x, y)
+ }
+ [U64(3), U64(n), x, y] => {
+ let x = cbor_value_to_dhall(&x)?;
+ let y = cbor_value_to_dhall(&y)?;
+ use BinOp::*;
+ let op = match n {
+ 0 => BoolOr,
+ 1 => BoolAnd,
+ 2 => BoolEQ,
+ 3 => BoolNE,
+ 4 => NaturalPlus,
+ 5 => NaturalTimes,
+ 6 => TextAppend,
+ 7 => ListAppend,
+ 8 => RecursiveRecordMerge,
+ 9 => RightBiasedRecordMerge,
+ 10 => RecursiveRecordTypeMerge,
+ 11 => ImportAlt,
+ 12 => Equivalence,
+ _ => {
+ Err(DecodeError::WrongFormatError("binop".to_owned()))?
+ }
+ };
+ BinOp(op, x, y)
+ }
+ [U64(4), t] => {
+ let t = cbor_value_to_dhall(&t)?;
+ EmptyListLit(rc(App(rc(ExprF::Builtin(Builtin::List)), t)))
+ }
+ [U64(4), Null, rest @ ..] => {
+ let rest = rest
+ .iter()
+ .map(cbor_value_to_dhall)
+ .collect::<Result<Vec<_>, _>>()?;
+ NEListLit(rest)
+ }
+ [U64(5), Null, x] => {
+ let x = cbor_value_to_dhall(&x)?;
+ SomeLit(x)
+ }
+ // Old-style optional literals
+ [U64(5), t] => {
+ let t = cbor_value_to_dhall(&t)?;
+ App(rc(ExprF::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)),
+ )
+ }
+ [U64(6), x, y] => {
+ let x = cbor_value_to_dhall(&x)?;
+ let y = cbor_value_to_dhall(&y)?;
+ Merge(x, y, None)
+ }
+ [U64(6), x, y, z] => {
+ let x = cbor_value_to_dhall(&x)?;
+ let y = cbor_value_to_dhall(&y)?;
+ let z = cbor_value_to_dhall(&z)?;
+ Merge(x, y, Some(z))
+ }
+ [U64(7), Object(map)] => {
+ let map = cbor_map_to_dhall_map(map)?;
+ RecordType(map)
+ }
+ [U64(8), Object(map)] => {
+ let map = cbor_map_to_dhall_map(map)?;
+ RecordLit(map)
+ }
+ [U64(9), x, String(l)] => {
+ let x = cbor_value_to_dhall(&x)?;
+ let l = Label::from(l.as_str());
+ Field(x, l)
+ }
+ [U64(10), x, Array(arr)] => {
+ let x = cbor_value_to_dhall(&x)?;
+ if let [y] = arr.as_slice() {
+ let y = cbor_value_to_dhall(&y)?;
+ ProjectionByExpr(x, y)
+ } else {
+ Err(DecodeError::WrongFormatError(
+ "projection-by-expr".to_owned(),
+ ))?
+ }
+ }
+ [U64(10), x, rest @ ..] => {
+ let x = cbor_value_to_dhall(&x)?;
+ let labels = rest
+ .iter()
+ .map(|s| match s {
+ String(s) => Ok(Label::from(s.as_str())),
+ _ => Err(DecodeError::WrongFormatError(
+ "projection".to_owned(),
+ )),
+ })
+ .collect::<Result<_, _>>()?;
+ Projection(x, labels)
+ }
+ [U64(11), Object(map)] => {
+ let map = cbor_map_to_dhall_opt_map(map)?;
+ UnionType(map)
+ }
+ [U64(12), ..] => Err(DecodeError::WrongFormatError(
+ "Union literals are not supported anymore".to_owned(),
+ ))?,
+ [U64(14), x, y, z] => {
+ let x = cbor_value_to_dhall(&x)?;
+ let y = cbor_value_to_dhall(&y)?;
+ let z = cbor_value_to_dhall(&z)?;
+ BoolIf(x, y, z)
+ }
+ [U64(15), U64(x)] => NaturalLit(*x as Natural),
+ [U64(16), U64(x)] => IntegerLit(*x as Integer),
+ [U64(16), I64(x)] => IntegerLit(*x as Integer),
+ [U64(18), String(first), rest @ ..] => {
+ TextLit(InterpolatedText::from((
+ first.clone(),
+ rest.iter()
+ .tuples()
+ .map(|(x, y)| {
+ let x = cbor_value_to_dhall(&x)?;
+ let y = match y {
+ String(s) => s.clone(),
+ _ => Err(DecodeError::WrongFormatError(
+ "text".to_owned(),
+ ))?,
+ };
+ Ok((x, y))
+ })
+ .collect::<Result<_, _>>()?,
+ )))
+ }
+ [U64(19), t] => {
+ let t = cbor_value_to_dhall(&t)?;
+ Assert(t)
+ }
+ [U64(24), hash, U64(mode), U64(scheme), rest @ ..] => {
+ let mode = match mode {
+ 0 => ImportMode::Code,
+ 1 => ImportMode::RawText,
+ 2 => ImportMode::Location,
+ _ => Err(DecodeError::WrongFormatError(format!(
+ "import/mode/unknown_mode: {:?}",
+ mode
+ )))?,
+ };
+ let hash = match hash {
+ Null => None,
+ Bytes(bytes) => match bytes.as_slice() {
+ [18, 32, rest @ ..] => {
+ Some(Hash::SHA256(rest.to_vec()))
+ }
+ _ => Err(DecodeError::WrongFormatError(format!(
+ "import/hash/unknown_multihash: {:?}",
+ bytes
+ )))?,
+ },
+ _ => Err(DecodeError::WrongFormatError(
+ "import/hash/should_be_bytes".to_owned(),
+ ))?,
+ };
+ let mut rest = rest.iter();
+ let location = match scheme {
+ 0 | 1 => {
+ let scheme = match scheme {
+ 0 => Scheme::HTTP,
+ _ => Scheme::HTTPS,
+ };
+ let headers = match rest.next() {
+ Some(Null) => None,
+ Some(x) => {
+ let x = cbor_value_to_dhall(&x)?;
+ Some(x)
+ }
+ _ => Err(DecodeError::WrongFormatError(
+ "import/remote/headers".to_owned(),
+ ))?,
+ };
+ let authority = match rest.next() {
+ Some(String(s)) => s.to_owned(),
+ _ => Err(DecodeError::WrongFormatError(
+ "import/remote/authority".to_owned(),
+ ))?,
+ };
+ let query = match rest.next_back() {
+ Some(Null) => None,
+ Some(String(s)) => Some(s.to_owned()),
+ _ => Err(DecodeError::WrongFormatError(
+ "import/remote/query".to_owned(),
+ ))?,
+ };
+ let file_path = rest
+ .map(|s| match s.as_string() {
+ Some(s) => Ok(s.clone()),
+ None => Err(DecodeError::WrongFormatError(
+ "import/remote/path".to_owned(),
+ )),
+ })
+ .collect::<Result<_, _>>()?;
+ let path = FilePath { file_path };
+ ImportLocation::Remote(URL {
+ scheme,
+ authority,
+ path,
+ query,
+ headers,
+ })
+ }
+ 2 | 3 | 4 | 5 => {
+ let prefix = match scheme {
+ 2 => FilePrefix::Absolute,
+ 3 => FilePrefix::Here,
+ 4 => FilePrefix::Parent,
+ 5 => FilePrefix::Home,
+ _ => Err(DecodeError::WrongFormatError(
+ "import/local/prefix".to_owned(),
+ ))?,
+ };
+ let file_path = rest
+ .map(|s| match s.as_string() {
+ Some(s) => Ok(s.clone()),
+ None => Err(DecodeError::WrongFormatError(
+ "import/local/path".to_owned(),
+ )),
+ })
+ .collect::<Result<_, _>>()?;
+ let path = FilePath { file_path };
+ ImportLocation::Local(prefix, path)
+ }
+ 6 => {
+ let env = match rest.next() {
+ Some(String(s)) => s.to_owned(),
+ _ => Err(DecodeError::WrongFormatError(
+ "import/env".to_owned(),
+ ))?,
+ };
+ ImportLocation::Env(env)
+ }
+ 7 => ImportLocation::Missing,
+ _ => Err(DecodeError::WrongFormatError(
+ "import/type".to_owned(),
+ ))?,
+ };
+ Import(crate::syntax::Import {
+ mode,
+ hash,
+ location,
+ })
+ }
+ [U64(25), bindings @ ..] => {
+ let mut tuples = bindings.iter().tuples();
+ let bindings = (&mut tuples)
+ .map(|(x, t, v)| {
+ let x = x.as_string().ok_or_else(|| {
+ DecodeError::WrongFormatError(
+ "let/label".to_owned(),
+ )
+ })?;
+ let x = Label::from(x.as_str());
+ let t = match t {
+ Null => None,
+ t => Some(cbor_value_to_dhall(&t)?),
+ };
+ let v = cbor_value_to_dhall(&v)?;
+ Ok((x, t, v))
+ })
+ .collect::<Result<Vec<_>, _>>()?;
+ let expr = tuples.into_buffer().next().ok_or_else(|| {
+ DecodeError::WrongFormatError("let/expr".to_owned())
+ })?;
+ let expr = cbor_value_to_dhall(expr)?;
+ return Ok(bindings
+ .into_iter()
+ .rev()
+ .fold(expr, |acc, (x, t, v)| rc(Let(x, t, v, acc))));
+ }
+ [U64(26), x, y] => {
+ let x = cbor_value_to_dhall(&x)?;
+ let y = cbor_value_to_dhall(&y)?;
+ Annot(x, y)
+ }
+ [U64(27), x] => {
+ let x = cbor_value_to_dhall(&x)?;
+ ToMap(x, None)
+ }
+ [U64(27), x, y] => {
+ let x = cbor_value_to_dhall(&x)?;
+ let y = cbor_value_to_dhall(&y)?;
+ ToMap(x, Some(y))
+ }
+ [U64(28), x] => {
+ let x = cbor_value_to_dhall(&x)?;
+ EmptyListLit(x)
+ }
+ _ => Err(DecodeError::WrongFormatError(format!("{:?}", data)))?,
+ },
+ _ => Err(DecodeError::WrongFormatError(format!("{:?}", data)))?,
+ }))
+}
+
+fn cbor_map_to_dhall_map<'a, T>(
+ map: impl IntoIterator<Item = (&'a cbor::ObjectKey, &'a cbor::Value)>,
+) -> Result<T, DecodeError>
+where
+ T: FromIterator<(Label, DecodedExpr)>,
+{
+ map.into_iter()
+ .map(|(k, v)| -> Result<(_, _), _> {
+ let k = k.as_string().ok_or_else(|| {
+ DecodeError::WrongFormatError("map/key".to_owned())
+ })?;
+ let v = cbor_value_to_dhall(v)?;
+ Ok((Label::from(k.as_ref()), v))
+ })
+ .collect::<Result<_, _>>()
+}
+
+fn cbor_map_to_dhall_opt_map<'a, T>(
+ map: impl IntoIterator<Item = (&'a cbor::ObjectKey, &'a cbor::Value)>,
+) -> Result<T, DecodeError>
+where
+ T: FromIterator<(Label, Option<DecodedExpr>)>,
+{
+ map.into_iter()
+ .map(|(k, v)| -> Result<(_, _), _> {
+ let k = k.as_string().ok_or_else(|| {
+ DecodeError::WrongFormatError("map/key".to_owned())
+ })?;
+ let v = match v {
+ cbor::Value::Null => None,
+ _ => Some(cbor_value_to_dhall(v)?),
+ };
+ Ok((Label::from(k.as_ref()), v))
+ })
+ .collect::<Result<_, _>>()
+}
+
+enum Serialize<'a, E> {
+ Expr(&'a Expr<E>),
+ CBOR(cbor::Value),
+ RecordMap(&'a DupTreeMap<Label, Expr<E>>),
+ UnionMap(&'a DupTreeMap<Label, Option<Expr<E>>>),
+}
+
+macro_rules! count {
+ (@replace_with $_t:tt $sub:expr) => { $sub };
+ ($($tts:tt)*) => {0usize $(+ count!(@replace_with $tts 1usize))*};
+}
+
+macro_rules! ser_seq {
+ ($ser:expr; $($elt:expr),* $(,)?) => {{
+ use serde::ser::SerializeSeq;
+ let count = count!($($elt)*);
+ let mut ser_seq = $ser.serialize_seq(Some(count))?;
+ $(
+ ser_seq.serialize_element(&$elt)?;
+ )*
+ ser_seq.end()
+ }};
+}
+
+fn serialize_subexpr<S, E>(ser: S, e: &Expr<E>) -> Result<S::Ok, S::Error>
+where
+ S: serde::ser::Serializer,
+{
+ use cbor::Value::{String, I64, U64};
+ use crate::syntax::Builtin;
+ use crate::syntax::ExprF::*;
+ use std::iter::once;
+
+ use self::Serialize::{RecordMap, UnionMap};
+ fn expr<E>(x: &Expr<E>) -> self::Serialize<'_, E> {
+ self::Serialize::Expr(x)
+ }
+ let cbor =
+ |v: cbor::Value| -> self::Serialize<'_, E> { self::Serialize::CBOR(v) };
+ let tag = |x: u64| cbor(U64(x));
+ let null = || cbor(cbor::Value::Null);
+ let label = |l: &Label| cbor(cbor::Value::String(l.into()));
+
+ match e.as_ref() {
+ Const(c) => ser.serialize_str(&c.to_string()),
+ Builtin(b) => ser.serialize_str(&b.to_string()),
+ BoolLit(b) => ser.serialize_bool(*b),
+ NaturalLit(n) => ser_seq!(ser; tag(15), U64(*n as u64)),
+ IntegerLit(n) => ser_seq!(ser; tag(16), I64(*n as i64)),
+ DoubleLit(n) => {
+ let n: f64 = (*n).into();
+ ser.serialize_f64(n)
+ }
+ BoolIf(x, y, z) => ser_seq!(ser; tag(14), expr(x), expr(y), expr(z)),
+ Var(V(l, n)) if l == &"_".into() => ser.serialize_u64(*n as u64),
+ Var(V(l, n)) => ser_seq!(ser; label(l), U64(*n as u64)),
+ Lam(l, x, y) if l == &"_".into() => {
+ ser_seq!(ser; tag(1), expr(x), expr(y))
+ }
+ Lam(l, x, y) => ser_seq!(ser; tag(1), label(l), expr(x), expr(y)),
+ Pi(l, x, y) if l == &"_".into() => {
+ ser_seq!(ser; tag(2), expr(x), expr(y))
+ }
+ Pi(l, x, y) => ser_seq!(ser; tag(2), label(l), expr(x), expr(y)),
+ Let(_, _, _, _) => {
+ let (bound_e, bindings) = collect_nested_lets(e);
+ let count = 1 + 3 * bindings.len() + 1;
+
+ use serde::ser::SerializeSeq;
+ let mut ser_seq = ser.serialize_seq(Some(count))?;
+ ser_seq.serialize_element(&tag(25))?;
+ for (l, t, v) in bindings {
+ ser_seq.serialize_element(&label(l))?;
+ match t {
+ Some(t) => ser_seq.serialize_element(&expr(t))?,
+ None => ser_seq.serialize_element(&null())?,
+ }
+ ser_seq.serialize_element(&expr(v))?;
+ }
+ ser_seq.serialize_element(&expr(bound_e))?;
+ ser_seq.end()
+ }
+ App(_, _) => {
+ let (f, args) = collect_nested_applications(e);
+ ser.collect_seq(
+ once(tag(0))
+ .chain(once(expr(f)))
+ .chain(args.into_iter().rev().map(expr)),
+ )
+ }
+ Annot(x, y) => ser_seq!(ser; tag(26), expr(x), expr(y)),
+ Assert(x) => ser_seq!(ser; tag(19), expr(x)),
+ 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)),
+ _ => ser_seq!(ser; tag(28), expr(x)),
+ },
+ _ => ser_seq!(ser; tag(28), expr(x)),
+ },
+ NEListLit(xs) => ser.collect_seq(
+ once(tag(4)).chain(once(null())).chain(xs.iter().map(expr)),
+ ),
+ TextLit(xs) => {
+ use crate::syntax::InterpolatedTextContents::{Expr, Text};
+ ser.collect_seq(once(tag(18)).chain(xs.iter().map(|x| match x {
+ Expr(x) => expr(x),
+ Text(x) => cbor(String(x.clone())),
+ })))
+ }
+ RecordType(map) => ser_seq!(ser; tag(7), RecordMap(map)),
+ RecordLit(map) => ser_seq!(ser; tag(8), RecordMap(map)),
+ UnionType(map) => ser_seq!(ser; tag(11), UnionMap(map)),
+ Field(x, l) => ser_seq!(ser; tag(9), expr(x), label(l)),
+ BinOp(op, x, y) => {
+ use crate::syntax::BinOp::*;
+ let op = match op {
+ BoolOr => 0,
+ BoolAnd => 1,
+ BoolEQ => 2,
+ BoolNE => 3,
+ NaturalPlus => 4,
+ NaturalTimes => 5,
+ TextAppend => 6,
+ ListAppend => 7,
+ RecursiveRecordMerge => 8,
+ RightBiasedRecordMerge => 9,
+ RecursiveRecordTypeMerge => 10,
+ ImportAlt => 11,
+ Equivalence => 12,
+ };
+ ser_seq!(ser; tag(3), U64(op), expr(x), expr(y))
+ }
+ Merge(x, y, None) => ser_seq!(ser; tag(6), expr(x), expr(y)),
+ Merge(x, y, Some(z)) => {
+ ser_seq!(ser; tag(6), expr(x), expr(y), expr(z))
+ }
+ ToMap(x, None) => ser_seq!(ser; tag(27), expr(x)),
+ ToMap(x, Some(y)) => ser_seq!(ser; tag(27), expr(x), expr(y)),
+ Projection(x, ls) => ser.collect_seq(
+ once(tag(10))
+ .chain(once(expr(x)))
+ .chain(ls.iter().map(label)),
+ ),
+ ProjectionByExpr(x, y) => {
+ ser_seq!(ser; tag(10), expr(x), vec![expr(y)])
+ }
+ Import(import) => serialize_import(ser, import),
+ Embed(_) => unimplemented!(
+ "An expression with resolved imports cannot be binary-encoded"
+ ),
+ }
+}
+
+fn serialize_import<S, E>(
+ ser: S,
+ import: &Import<Expr<E>>,
+) -> Result<S::Ok, S::Error>
+where
+ S: serde::ser::Serializer,
+{
+ use cbor::Value::{Bytes, Null, U64};
+ use serde::ser::SerializeSeq;
+
+ let count = 4 + match &import.location {
+ ImportLocation::Remote(url) => 3 + url.path.file_path.len(),
+ ImportLocation::Local(_, path) => path.file_path.len(),
+ ImportLocation::Env(_) => 1,
+ ImportLocation::Missing => 0,
+ };
+ let mut ser_seq = ser.serialize_seq(Some(count))?;
+
+ ser_seq.serialize_element(&U64(24))?;
+
+ let hash = match &import.hash {
+ None => Null,
+ Some(Hash::SHA256(h)) => {
+ let mut bytes = vec![18, 32];
+ bytes.extend_from_slice(h);
+ Bytes(bytes)
+ }
+ };
+ ser_seq.serialize_element(&hash)?;
+
+ let mode = match import.mode {
+ ImportMode::Code => 0,
+ ImportMode::RawText => 1,
+ ImportMode::Location => 2,
+ };
+ ser_seq.serialize_element(&U64(mode))?;
+
+ let scheme = match &import.location {
+ ImportLocation::Remote(url) => match url.scheme {
+ Scheme::HTTP => 0,
+ Scheme::HTTPS => 1,
+ },
+ ImportLocation::Local(prefix, _) => match prefix {
+ FilePrefix::Absolute => 2,
+ FilePrefix::Here => 3,
+ FilePrefix::Parent => 4,
+ FilePrefix::Home => 5,
+ },
+ ImportLocation::Env(_) => 6,
+ ImportLocation::Missing => 7,
+ };
+ ser_seq.serialize_element(&U64(scheme))?;
+
+ match &import.location {
+ ImportLocation::Remote(url) => {
+ match &url.headers {
+ None => ser_seq.serialize_element(&Null)?,
+ Some(e) => {
+ ser_seq.serialize_element(&self::Serialize::Expr(e))?
+ }
+ };
+ ser_seq.serialize_element(&url.authority)?;
+ for p in url.path.file_path.iter() {
+ ser_seq.serialize_element(&p)?;
+ }
+ match &url.query {
+ None => ser_seq.serialize_element(&Null)?,
+ Some(x) => ser_seq.serialize_element(x)?,
+ };
+ }
+ ImportLocation::Local(_, path) => {
+ for p in path.file_path.iter() {
+ ser_seq.serialize_element(&p)?;
+ }
+ }
+ ImportLocation::Env(env) => {
+ ser_seq.serialize_element(env)?;
+ }
+ ImportLocation::Missing => {}
+ }
+
+ ser_seq.end()
+}
+
+impl<'a, E> serde::ser::Serialize for Serialize<'a, E> {
+ fn serialize<S>(&self, ser: S) -> Result<S::Ok, S::Error>
+ where
+ S: serde::ser::Serializer,
+ {
+ match self {
+ Serialize::Expr(e) => serialize_subexpr(ser, e),
+ Serialize::CBOR(v) => v.serialize(ser),
+ Serialize::RecordMap(map) => {
+ ser.collect_map(map.iter().map(|(k, v)| {
+ (cbor::Value::String(k.into()), Serialize::Expr(v))
+ }))
+ }
+ Serialize::UnionMap(map) => {
+ ser.collect_map(map.iter().map(|(k, v)| {
+ let v = match v {
+ Some(x) => Serialize::Expr(x),
+ None => Serialize::CBOR(cbor::Value::Null),
+ };
+ (cbor::Value::String(k.into()), v)
+ }))
+ }
+ }
+ }
+}
+
+fn collect_nested_applications<'a, E>(
+ e: &'a Expr<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) => {
+ vec.push(a);
+ go(f, vec)
+ }
+ _ => e,
+ }
+ }
+ let mut vec = vec![];
+ let e = go(e, &mut vec);
+ (e, vec)
+}
+
+type LetBinding<'a, E> = (&'a Label, &'a Option<Expr<E>>, &'a Expr<E>);
+
+fn collect_nested_lets<'a, E>(
+ e: &'a Expr<E>,
+) -> (&'a Expr<E>, Vec<LetBinding<'a, E>>) {
+ fn go<'a, E>(
+ e: &'a Expr<E>,
+ vec: &mut Vec<LetBinding<'a, E>>,
+ ) -> &'a Expr<E> {
+ match e.as_ref() {
+ ExprF::Let(l, t, v, e) => {
+ vec.push((l, t, v));
+ go(e, vec)
+ }
+ _ => e,
+ }
+ }
+ let mut vec = vec![];
+ let e = go(e, &mut vec);
+ (e, vec)
+}
diff --git a/dhall/src/semantics/phase/mod.rs b/dhall/src/semantics/phase/mod.rs
new file mode 100644
index 0000000..918c4d0
--- /dev/null
+++ b/dhall/src/semantics/phase/mod.rs
@@ -0,0 +1,254 @@
+use std::fmt::Display;
+use std::path::Path;
+
+use crate::syntax::{Builtin, Const, Expr};
+
+use crate::core::value::{ToExprOptions, Value};
+use crate::core::valuef::ValueF;
+use crate::core::var::{AlphaVar, Shift, Subst};
+use crate::error::{EncodeError, Error, ImportError, TypeError};
+
+use resolve::ImportRoot;
+
+pub(crate) mod binary;
+pub(crate) mod normalize;
+pub(crate) mod parse;
+pub(crate) mod resolve;
+pub(crate) mod typecheck;
+
+pub type ParsedExpr = Expr<Normalized>;
+pub type DecodedExpr = Expr<Normalized>;
+pub type ResolvedExpr = Expr<Normalized>;
+pub type NormalizedExpr = Expr<Normalized>;
+
+#[derive(Debug, Clone)]
+pub struct Parsed(ParsedExpr, ImportRoot);
+
+/// An expression where all imports have been resolved
+///
+/// Invariant: there must be no `Import` nodes or `ImportAlt` operations left.
+#[derive(Debug, Clone)]
+pub struct Resolved(ResolvedExpr);
+
+/// A typed expression
+#[derive(Debug, Clone)]
+pub struct Typed(Value);
+
+/// A normalized expression.
+///
+/// Invariant: the contained Typed expression must be in normal form,
+#[derive(Debug, Clone)]
+pub struct Normalized(Typed);
+
+impl Parsed {
+ pub fn parse_file(f: &Path) -> Result<Parsed, Error> {
+ parse::parse_file(f)
+ }
+ pub fn parse_str(s: &str) -> Result<Parsed, Error> {
+ parse::parse_str(s)
+ }
+ pub fn parse_binary_file(f: &Path) -> Result<Parsed, Error> {
+ parse::parse_binary_file(f)
+ }
+ pub fn parse_binary(data: &[u8]) -> Result<Parsed, Error> {
+ parse::parse_binary(data)
+ }
+
+ pub fn resolve(self) -> Result<Resolved, ImportError> {
+ resolve::resolve(self)
+ }
+ pub fn skip_resolve(self) -> Result<Resolved, ImportError> {
+ resolve::skip_resolve_expr(self)
+ }
+
+ pub fn encode(&self) -> Result<Vec<u8>, EncodeError> {
+ crate::phase::binary::encode(&self.0)
+ }
+}
+
+impl Resolved {
+ pub fn typecheck(self) -> Result<Typed, TypeError> {
+ Ok(typecheck::typecheck(self.0)?.into_typed())
+ }
+ pub fn typecheck_with(self, ty: &Typed) -> Result<Typed, TypeError> {
+ Ok(typecheck::typecheck_with(self.0, ty.normalize_to_expr())?
+ .into_typed())
+ }
+}
+
+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)
+ }
+
+ 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_value(th: Value) -> Self {
+ Typed(th)
+ }
+ pub(crate) fn const_type() -> Self {
+ Typed::from_const(Const::Type)
+ }
+
+ pub(crate) fn to_expr(&self) -> NormalizedExpr {
+ self.0.to_expr(ToExprOptions {
+ alpha: false,
+ normalize: false,
+ })
+ }
+ pub fn normalize_to_expr(&self) -> NormalizedExpr {
+ self.0.to_expr(ToExprOptions {
+ alpha: false,
+ normalize: true,
+ })
+ }
+ pub(crate) fn normalize_to_expr_alpha(&self) -> NormalizedExpr {
+ self.0.to_expr(ToExprOptions {
+ alpha: true,
+ normalize: true,
+ })
+ }
+ pub(crate) fn to_value(&self) -> Value {
+ self.0.clone()
+ }
+ pub(crate) fn into_value(self) -> Value {
+ self.0
+ }
+
+ pub(crate) fn normalize_mut(&mut self) {
+ self.0.normalize_mut()
+ }
+
+ pub(crate) fn get_type(&self) -> Result<Typed, TypeError> {
+ Ok(self.0.get_type()?.into_typed())
+ }
+
+ pub fn make_builtin_type(b: Builtin) -> Self {
+ Typed::from_value(Value::from_builtin(b))
+ }
+ pub fn make_optional_type(t: Typed) -> Self {
+ Typed::from_value(
+ Value::from_builtin(Builtin::Optional).app(t.to_value()),
+ )
+ }
+ pub fn make_list_type(t: Typed) -> Self {
+ Typed::from_value(Value::from_builtin(Builtin::List).app(t.to_value()))
+ }
+ pub fn make_record_type(
+ kts: impl Iterator<Item = (String, Typed)>,
+ ) -> Self {
+ Typed::from_valuef_and_type(
+ ValueF::RecordType(
+ kts.map(|(k, t)| (k.into(), t.into_value())).collect(),
+ ),
+ Typed::const_type(),
+ )
+ }
+ pub fn make_union_type(
+ kts: impl Iterator<Item = (String, Option<Typed>)>,
+ ) -> Self {
+ Typed::from_valuef_and_type(
+ ValueF::UnionType(
+ kts.map(|(k, t)| (k.into(), t.map(|t| t.into_value())))
+ .collect(),
+ ),
+ Typed::const_type(),
+ )
+ }
+}
+
+impl Normalized {
+ pub fn encode(&self) -> Result<Vec<u8>, EncodeError> {
+ crate::phase::binary::encode(&self.to_expr())
+ }
+
+ pub(crate) fn to_expr(&self) -> NormalizedExpr {
+ self.0.normalize_to_expr()
+ }
+ pub(crate) fn to_expr_alpha(&self) -> NormalizedExpr {
+ self.0.normalize_to_expr_alpha()
+ }
+ pub(crate) fn into_typed(self) -> Typed {
+ self.0
+ }
+}
+
+impl Shift for Typed {
+ fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> {
+ Some(Typed(self.0.shift(delta, var)?))
+ }
+}
+
+impl Shift for Normalized {
+ fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> {
+ Some(Normalized(self.0.shift(delta, var)?))
+ }
+}
+
+impl Subst<Value> for Typed {
+ fn subst_shift(&self, var: &AlphaVar, val: &Value) -> Self {
+ Typed(self.0.subst_shift(var, val))
+ }
+}
+
+macro_rules! derive_traits_for_wrapper_struct {
+ ($ty:ident) => {
+ impl std::cmp::PartialEq for $ty {
+ fn eq(&self, other: &Self) -> bool {
+ self.0 == other.0
+ }
+ }
+
+ impl std::cmp::Eq for $ty {}
+
+ impl std::fmt::Display for $ty {
+ fn fmt(
+ &self,
+ f: &mut std::fmt::Formatter,
+ ) -> Result<(), std::fmt::Error> {
+ self.0.fmt(f)
+ }
+ }
+ };
+}
+
+derive_traits_for_wrapper_struct!(Parsed);
+derive_traits_for_wrapper_struct!(Resolved);
+derive_traits_for_wrapper_struct!(Normalized);
+
+impl std::hash::Hash for Normalized {
+ fn hash<H>(&self, state: &mut H)
+ where
+ H: std::hash::Hasher,
+ {
+ if let Ok(vec) = self.encode() {
+ vec.hash(state)
+ }
+ }
+}
+
+impl Eq for Typed {}
+impl PartialEq for Typed {
+ fn eq(&self, other: &Self) -> bool {
+ self.0 == other.0
+ }
+}
+
+impl Display for Typed {
+ fn fmt(&self, f: &mut std::fmt::Formatter) -> Result<(), std::fmt::Error> {
+ self.to_expr().fmt(f)
+ }
+}
diff --git a/dhall/src/semantics/phase/normalize.rs b/dhall/src/semantics/phase/normalize.rs
new file mode 100644
index 0000000..3ed53f4
--- /dev/null
+++ b/dhall/src/semantics/phase/normalize.rs
@@ -0,0 +1,794 @@
+use std::collections::HashMap;
+
+use crate::syntax::Const::Type;
+use crate::syntax::{
+ BinOp, Builtin, ExprF, InterpolatedText, InterpolatedTextContents, Label,
+ NaiveDouble,
+};
+
+use crate::core::value::Value;
+use crate::core::valuef::ValueF;
+use crate::core::var::{AlphaLabel, Shift, Subst};
+use crate::phase::Normalized;
+
+// Ad-hoc macro to help construct closures
+macro_rules! make_closure {
+ (#$var:ident) => { $var.clone() };
+ (var($var:ident, $n:expr, $($ty:tt)*)) => {{
+ let var = crate::core::var::AlphaVar::from_var_and_alpha(
+ Label::from(stringify!($var)).into(),
+ $n
+ );
+ ValueF::Var(var)
+ .into_value_with_type(make_closure!($($ty)*))
+ }};
+ // Warning: assumes that $ty, as a dhall value, has type `Type`
+ (λ($var:ident : $($ty:tt)*) -> $($body:tt)*) => {{
+ let var: AlphaLabel = Label::from(stringify!($var)).into();
+ 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)
+ .into_value_with_type(Value::from_const(Type));
+ ValueF::Lam(var, ty, body).into_value_with_type(lam_ty)
+ }};
+ (Natural) => {
+ Value::from_builtin(Builtin::Natural)
+ };
+ (List $($rest:tt)*) => {
+ Value::from_builtin(Builtin::List)
+ .app(make_closure!($($rest)*))
+ };
+ (Some($($rest:tt)*)) => {{
+ 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)
+ }};
+ (1 + $($rest:tt)*) => {
+ ValueF::PartialExpr(ExprF::BinOp(
+ crate::syntax::BinOp::NaturalPlus,
+ make_closure!($($rest)*),
+ Value::from_valuef_and_type(
+ ValueF::NaturalLit(1),
+ make_closure!(Natural)
+ ),
+ )).into_value_with_type(
+ make_closure!(Natural)
+ )
+ };
+ ([ $($head:tt)* ] # $($tail:tt)*) => {{
+ let head = make_closure!($($head)*);
+ let tail = make_closure!($($tail)*);
+ let list_type = tail.get_type_not_sort();
+ ValueF::PartialExpr(ExprF::BinOp(
+ crate::syntax::BinOp::ListAppend,
+ ValueF::NEListLit(vec![head])
+ .into_value_with_type(list_type.clone()),
+ tail,
+ )).into_value_with_type(list_type)
+ }};
+}
+
+#[allow(clippy::cognitive_complexity)]
+pub(crate) fn apply_builtin(
+ b: Builtin,
+ args: Vec<Value>,
+ ty: &Value,
+) -> ValueF {
+ use crate::syntax::Builtin::*;
+ use ValueF::*;
+
+ // Small helper enum
+ enum Ret<'a> {
+ ValueF(ValueF),
+ Value(Value),
+ // For applications that can return a function, it's important to keep the remaining
+ // arguments to apply them to the resulting function.
+ ValueWithRemainingArgs(&'a [Value], Value),
+ DoneAsIs,
+ }
+
+ let ret = match (b, args.as_slice()) {
+ (OptionalNone, [t]) => Ret::ValueF(EmptyOptionalLit(t.clone())),
+ (NaturalIsZero, [n]) => match &*n.as_whnf() {
+ NaturalLit(n) => Ret::ValueF(BoolLit(*n == 0)),
+ _ => Ret::DoneAsIs,
+ },
+ (NaturalEven, [n]) => match &*n.as_whnf() {
+ NaturalLit(n) => Ret::ValueF(BoolLit(*n % 2 == 0)),
+ _ => Ret::DoneAsIs,
+ },
+ (NaturalOdd, [n]) => match &*n.as_whnf() {
+ NaturalLit(n) => Ret::ValueF(BoolLit(*n % 2 != 0)),
+ _ => Ret::DoneAsIs,
+ },
+ (NaturalToInteger, [n]) => match &*n.as_whnf() {
+ NaturalLit(n) => Ret::ValueF(IntegerLit(*n as isize)),
+ _ => Ret::DoneAsIs,
+ },
+ (NaturalShow, [n]) => match &*n.as_whnf() {
+ NaturalLit(n) => {
+ Ret::ValueF(TextLit(vec![InterpolatedTextContents::Text(
+ n.to_string(),
+ )]))
+ }
+ _ => 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 }))
+ }
+ (NaturalLit(0), _) => Ret::Value(b.clone()),
+ (_, NaturalLit(0)) => Ret::ValueF(NaturalLit(0)),
+ _ if a == b => Ret::ValueF(NaturalLit(0)),
+ _ => Ret::DoneAsIs,
+ },
+ (IntegerShow, [n]) => match &*n.as_whnf() {
+ IntegerLit(n) => {
+ let s = if *n < 0 {
+ n.to_string()
+ } else {
+ format!("+{}", n)
+ };
+ Ret::ValueF(TextLit(vec![InterpolatedTextContents::Text(s)]))
+ }
+ _ => Ret::DoneAsIs,
+ },
+ (IntegerToDouble, [n]) => match &*n.as_whnf() {
+ IntegerLit(n) => {
+ Ret::ValueF(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(),
+ )]))
+ }
+ _ => Ret::DoneAsIs,
+ },
+ (TextShow, [v]) => match &*v.as_whnf() {
+ TextLit(elts) => {
+ match elts.as_slice() {
+ // Empty string literal.
+ [] => {
+ // Printing InterpolatedText takes care of all the escaping
+ let txt: InterpolatedText<Normalized> =
+ std::iter::empty().collect();
+ let s = txt.to_string();
+ Ret::ValueF(TextLit(vec![
+ InterpolatedTextContents::Text(s),
+ ]))
+ }
+ // If there are no interpolations (invariants ensure that when there are no
+ // interpolations, there is a single Text item) in the literal.
+ [InterpolatedTextContents::Text(s)] => {
+ // Printing InterpolatedText takes care of all the escaping
+ let txt: InterpolatedText<Normalized> =
+ std::iter::once(InterpolatedTextContents::Text(
+ s.clone(),
+ ))
+ .collect();
+ let s = txt.to_string();
+ Ret::ValueF(TextLit(vec![
+ InterpolatedTextContents::Text(s),
+ ]))
+ }
+ _ => Ret::DoneAsIs,
+ }
+ }
+ _ => Ret::DoneAsIs,
+ },
+ (ListLength, [_, l]) => match &*l.as_whnf() {
+ EmptyListLit(_) => Ret::ValueF(NaturalLit(0)),
+ NEListLit(xs) => Ret::ValueF(NaturalLit(xs.len())),
+ _ => Ret::DoneAsIs,
+ },
+ (ListHead, [_, l]) => match &*l.as_whnf() {
+ EmptyListLit(n) => Ret::ValueF(EmptyOptionalLit(n.clone())),
+ NEListLit(xs) => {
+ Ret::ValueF(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(
+ xs.iter().rev().next().unwrap().clone(),
+ )),
+ _ => Ret::DoneAsIs,
+ },
+ (ListReverse, [_, l]) => match &*l.as_whnf() {
+ EmptyListLit(n) => Ret::ValueF(EmptyListLit(n.clone())),
+ NEListLit(xs) => {
+ Ret::ValueF(NEListLit(xs.iter().rev().cloned().collect()))
+ }
+ _ => Ret::DoneAsIs,
+ },
+ (ListIndexed, [_, l]) => {
+ let l_whnf = l.as_whnf();
+ match &*l_whnf {
+ EmptyListLit(_) | NEListLit(_) => {
+ // Extract the type of the list elements
+ let t = match &*l_whnf {
+ EmptyListLit(t) => t.clone(),
+ NEListLit(xs) => xs[0].get_type_not_sort(),
+ _ => unreachable!(),
+ };
+
+ // Construct the returned record type: { index: Natural, value: t }
+ 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(
+ RecordType(kts),
+ Value::from_const(Type),
+ );
+
+ // Construct the new list, with added indices
+ let list = match &*l_whnf {
+ EmptyListLit(_) => EmptyListLit(t),
+ NEListLit(xs) => NEListLit(
+ xs.iter()
+ .enumerate()
+ .map(|(i, e)| {
+ let mut kvs = HashMap::new();
+ kvs.insert(
+ "index".into(),
+ Value::from_valuef_and_type(
+ NaturalLit(i),
+ Value::from_builtin(
+ Builtin::Natural,
+ ),
+ ),
+ );
+ kvs.insert("value".into(), e.clone());
+ Value::from_valuef_and_type(
+ RecordLit(kvs),
+ t.clone(),
+ )
+ })
+ .collect(),
+ ),
+ _ => unreachable!(),
+ };
+ Ret::ValueF(list)
+ }
+ _ => Ret::DoneAsIs,
+ }
+ }
+ (ListBuild, [t, f]) => match &*f.as_whnf() {
+ // fold/build fusion
+ ValueF::AppliedBuiltin(ListFold, args) => {
+ if args.len() >= 2 {
+ Ret::Value(args[1].clone())
+ } else {
+ // Do we really need to handle this case ?
+ unimplemented!()
+ }
+ }
+ _ => {
+ let list_t = Value::from_builtin(List).app(t.clone());
+ Ret::Value(
+ f.app(list_t.clone())
+ .app({
+ // Move `t` under new variables
+ let t1 = t.under_binder(Label::from("x"));
+ let t2 = t1.under_binder(Label::from("xs"));
+ make_closure!(
+ λ(x : #t) ->
+ λ(xs : List #t1) ->
+ [ var(x, 1, #t2) ] # var(xs, 0, List #t2)
+ )
+ })
+ .app(
+ EmptyListLit(t.clone())
+ .into_value_with_type(list_t),
+ ),
+ )
+ }
+ },
+ (ListFold, [_, l, _, cons, nil, r @ ..]) => match &*l.as_whnf() {
+ EmptyListLit(_) => Ret::ValueWithRemainingArgs(r, nil.clone()),
+ NEListLit(xs) => {
+ let mut v = nil.clone();
+ for x in xs.iter().cloned().rev() {
+ v = cons.app(x).app(v);
+ }
+ Ret::ValueWithRemainingArgs(r, v)
+ }
+ _ => Ret::DoneAsIs,
+ },
+ (OptionalBuild, [t, f]) => match &*f.as_whnf() {
+ // fold/build fusion
+ ValueF::AppliedBuiltin(OptionalFold, args) => {
+ if args.len() >= 2 {
+ Ret::Value(args[1].clone())
+ } else {
+ // Do we really need to handle this case ?
+ unimplemented!()
+ }
+ }
+ _ => {
+ let optional_t = Value::from_builtin(Optional).app(t.clone());
+ Ret::Value(
+ f.app(optional_t.clone())
+ .app({
+ let t1 = t.under_binder(Label::from("x"));
+ make_closure!(λ(x: #t) -> Some(var(x, 0, #t1)))
+ })
+ .app(
+ EmptyOptionalLit(t.clone())
+ .into_value_with_type(optional_t),
+ ),
+ )
+ }
+ },
+ (OptionalFold, [_, v, _, just, nothing, r @ ..]) => match &*v.as_whnf()
+ {
+ EmptyOptionalLit(_) => {
+ Ret::ValueWithRemainingArgs(r, nothing.clone())
+ }
+ NEOptionalLit(x) => {
+ Ret::ValueWithRemainingArgs(r, just.app(x.clone()))
+ }
+ _ => Ret::DoneAsIs,
+ },
+ (NaturalBuild, [f]) => match &*f.as_whnf() {
+ // fold/build fusion
+ ValueF::AppliedBuiltin(NaturalFold, args) => {
+ if !args.is_empty() {
+ Ret::Value(args[0].clone())
+ } else {
+ // Do we really need to handle this case ?
+ unimplemented!()
+ }
+ }
+ _ => Ret::Value(
+ f.app(Value::from_builtin(Natural))
+ .app(make_closure!(
+ λ(x : Natural) -> 1 + var(x, 0, Natural)
+ ))
+ .app(
+ NaturalLit(0)
+ .into_value_with_type(Value::from_builtin(Natural)),
+ ),
+ ),
+ },
+ (NaturalFold, [n, t, succ, zero, r @ ..]) => match &*n.as_whnf() {
+ NaturalLit(0) => Ret::ValueWithRemainingArgs(r, zero.clone()),
+ NaturalLit(n) => {
+ let fold = Value::from_builtin(NaturalFold)
+ .app(
+ NaturalLit(n - 1)
+ .into_value_with_type(Value::from_builtin(Natural)),
+ )
+ .app(t.clone())
+ .app(succ.clone())
+ .app(zero.clone());
+ Ret::ValueWithRemainingArgs(r, succ.app(fold))
+ }
+ _ => Ret::DoneAsIs,
+ },
+ _ => Ret::DoneAsIs,
+ };
+ match ret {
+ Ret::ValueF(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();
+ for x in args.into_iter().skip(n_consumed_args) {
+ v = v.app(x);
+ }
+ v.to_whnf_check_type(ty)
+ }
+ Ret::DoneAsIs => AppliedBuiltin(b, args),
+ }
+}
+
+pub(crate) fn apply_any(f: Value, a: Value, ty: &Value) -> ValueF {
+ let f_borrow = f.as_whnf();
+ match &*f_borrow {
+ ValueF::Lam(x, _, e) => {
+ e.subst_shift(&x.into(), &a).to_whnf_check_type(ty)
+ }
+ ValueF::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())
+ }
+ _ => {
+ drop(f_borrow);
+ ValueF::PartialExpr(ExprF::App(f, a))
+ }
+ }
+}
+
+pub(crate) fn squash_textlit(
+ elts: impl Iterator<Item = InterpolatedTextContents<Value>>,
+) -> Vec<InterpolatedTextContents<Value>> {
+ use std::mem::replace;
+ use InterpolatedTextContents::{Expr, Text};
+
+ fn inner(
+ elts: impl Iterator<Item = InterpolatedTextContents<Value>>,
+ crnt_str: &mut String,
+ ret: &mut Vec<InterpolatedTextContents<Value>>,
+ ) {
+ for contents in elts {
+ match contents {
+ Text(s) => crnt_str.push_str(&s),
+ Expr(e) => {
+ let e_borrow = e.as_whnf();
+ match &*e_borrow {
+ ValueF::TextLit(elts2) => {
+ inner(elts2.iter().cloned(), crnt_str, ret)
+ }
+ _ => {
+ drop(e_borrow);
+ if !crnt_str.is_empty() {
+ ret.push(Text(replace(crnt_str, String::new())))
+ }
+ ret.push(Expr(e.clone()))
+ }
+ }
+ }
+ }
+ }
+ }
+
+ let mut crnt_str = String::new();
+ let mut ret = Vec::new();
+ inner(elts, &mut crnt_str, &mut ret);
+ if !crnt_str.is_empty() {
+ ret.push(Text(replace(&mut crnt_str, String::new())))
+ }
+ ret
+}
+
+pub(crate) fn merge_maps<K, V, F, Err>(
+ map1: &HashMap<K, V>,
+ map2: &HashMap<K, V>,
+ mut f: F,
+) -> Result<HashMap<K, V>, Err>
+where
+ F: FnMut(&K, &V, &V) -> Result<V, Err>,
+ K: std::hash::Hash + Eq + Clone,
+ V: Clone,
+{
+ let mut kvs = HashMap::new();
+ for (x, v2) in map2 {
+ let newv = if let Some(v1) = map1.get(x) {
+ f(x, v1, v2)?
+ } else {
+ v2.clone()
+ };
+ kvs.insert(x.clone(), newv);
+ }
+ for (x, v1) in map1 {
+ // Insert only if key not already present
+ kvs.entry(x.clone()).or_insert_with(|| v1.clone());
+ }
+ Ok(kvs)
+}
+
+// Small helper enum to avoid repetition
+enum Ret<'a> {
+ ValueF(ValueF),
+ Value(Value),
+ ValueRef(&'a Value),
+ Expr(ExprF<Value, Normalized>),
+}
+
+fn apply_binop<'a>(
+ o: BinOp,
+ x: &'a Value,
+ y: &'a Value,
+ ty: &Value,
+) -> Option<Ret<'a>> {
+ use BinOp::{
+ BoolAnd, BoolEQ, BoolNE, BoolOr, Equivalence, ListAppend, NaturalPlus,
+ NaturalTimes, RecursiveRecordMerge, RecursiveRecordTypeMerge,
+ RightBiasedRecordMerge, TextAppend,
+ };
+ use ValueF::{
+ BoolLit, EmptyListLit, NEListLit, NaturalLit, RecordLit, RecordType,
+ TextLit,
+ };
+ let x_borrow = x.as_whnf();
+ let y_borrow = y.as_whnf();
+ 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, _, _) if x == y => Ret::ValueRef(x),
+ (BoolOr, BoolLit(true), _) => Ret::ValueF(BoolLit(true)),
+ (BoolOr, _, BoolLit(true)) => Ret::ValueF(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)),
+ (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)),
+
+ (NaturalPlus, NaturalLit(0), _) => Ret::ValueRef(y),
+ (NaturalPlus, _, NaturalLit(0)) => Ret::ValueRef(x),
+ (NaturalPlus, NaturalLit(x), NaturalLit(y)) => {
+ Ret::ValueF(NaturalLit(x + y))
+ }
+ (NaturalTimes, NaturalLit(0), _) => Ret::ValueF(NaturalLit(0)),
+ (NaturalTimes, _, NaturalLit(0)) => Ret::ValueF(NaturalLit(0)),
+ (NaturalTimes, NaturalLit(1), _) => Ret::ValueRef(y),
+ (NaturalTimes, _, NaturalLit(1)) => Ret::ValueRef(x),
+ (NaturalTimes, NaturalLit(x), NaturalLit(y)) => {
+ Ret::ValueF(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(),
+ )),
+
+ (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(
+ 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(
+ x.iter().cloned().chain(once(y)),
+ )))
+ }
+ (TextAppend, _, TextLit(y)) => {
+ use std::iter::once;
+ let x = InterpolatedTextContents::Expr(x.clone());
+ Ret::ValueF(TextLit(squash_textlit(
+ once(x).chain(y.iter().cloned()),
+ )))
+ }
+
+ (RightBiasedRecordMerge, _, RecordLit(kvs)) if kvs.is_empty() => {
+ Ret::ValueRef(x)
+ }
+ (RightBiasedRecordMerge, RecordLit(kvs), _) if kvs.is_empty() => {
+ Ret::ValueRef(y)
+ }
+ (RightBiasedRecordMerge, RecordLit(kvs1), RecordLit(kvs2)) => {
+ let mut kvs = kvs2.clone();
+ for (x, v) in kvs1 {
+ // Insert only if key not already present
+ kvs.entry(x.clone()).or_insert_with(|| v.clone());
+ }
+ Ret::ValueF(RecordLit(kvs))
+ }
+
+ (RecursiveRecordMerge, _, RecordLit(kvs)) if kvs.is_empty() => {
+ Ret::ValueRef(x)
+ }
+ (RecursiveRecordMerge, RecordLit(kvs), _) if kvs.is_empty() => {
+ Ret::ValueRef(y)
+ }
+ (RecursiveRecordMerge, RecordLit(kvs1), RecordLit(kvs2)) => {
+ let ty_borrow = ty.as_whnf();
+ let kts = match &*ty_borrow {
+ RecordType(kts) => kts,
+ _ => unreachable!("Internal type error"),
+ };
+ let kvs = merge_maps::<_, _, _, !>(kvs1, kvs2, |k, v1, v2| {
+ Ok(Value::from_valuef_and_type(
+ ValueF::PartialExpr(ExprF::BinOp(
+ RecursiveRecordMerge,
+ v1.clone(),
+ v2.clone(),
+ )),
+ kts.get(k).expect("Internal type error").clone(),
+ ))
+ })?;
+ Ret::ValueF(RecordLit(kvs))
+ }
+
+ (RecursiveRecordTypeMerge, _, _) | (Equivalence, _, _) => {
+ unreachable!("This case should have been handled in typecheck")
+ }
+
+ _ => return None,
+ })
+}
+
+pub(crate) fn normalize_one_layer(
+ expr: ExprF<Value, Normalized>,
+ ty: &Value,
+) -> ValueF {
+ use ValueF::{
+ AppliedBuiltin, BoolLit, DoubleLit, EmptyListLit, IntegerLit,
+ NEListLit, NEOptionalLit, NaturalLit, RecordLit, TextLit,
+ UnionConstructor, UnionLit, UnionType,
+ };
+
+ let ret = match expr {
+ ExprF::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(_) => {
+ 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) => {
+ // 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()))
+ }
+ _ => {
+ drop(t_borrow);
+ Ret::Expr(expr)
+ }
+ }
+ }
+ ExprF::NEListLit(elts) => {
+ Ret::ValueF(NEListLit(elts.into_iter().collect()))
+ }
+ ExprF::RecordLit(kvs) => {
+ Ret::ValueF(RecordLit(kvs.into_iter().collect()))
+ }
+ ExprF::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))
+ }
+ }
+ ExprF::BoolIf(ref b, ref e1, ref e2) => {
+ let b_borrow = b.as_whnf();
+ match &*b_borrow {
+ BoolLit(true) => Ret::ValueRef(e1),
+ BoolLit(false) => Ret::ValueRef(e2),
+ _ => {
+ let e1_borrow = e1.as_whnf();
+ let e2_borrow = e2.as_whnf();
+ match (&*e1_borrow, &*e2_borrow) {
+ // Simplify `if b then True else False`
+ (BoolLit(true), BoolLit(false)) => Ret::ValueRef(b),
+ _ if e1 == e2 => Ret::ValueRef(e1),
+ _ => {
+ drop(b_borrow);
+ drop(e1_borrow);
+ drop(e2_borrow);
+ Ret::Expr(expr)
+ }
+ }
+ }
+ }
+ }
+ ExprF::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()))
+ }
+ ExprF::Projection(ref v, ref ls) => {
+ let v_borrow = v.as_whnf();
+ match &*v_borrow {
+ RecordLit(kvs) => Ret::ValueF(RecordLit(
+ ls.iter()
+ .filter_map(|l| {
+ kvs.get(l).map(|x| (l.clone(), x.clone()))
+ })
+ .collect(),
+ )),
+ _ => {
+ drop(v_borrow);
+ Ret::Expr(expr)
+ }
+ }
+ }
+ ExprF::Field(ref v, ref l) => {
+ let v_borrow = v.as_whnf();
+ match &*v_borrow {
+ RecordLit(kvs) => match kvs.get(l) {
+ Some(r) => Ret::Value(r.clone()),
+ None => {
+ drop(v_borrow);
+ Ret::Expr(expr)
+ }
+ },
+ UnionType(kts) => {
+ Ret::ValueF(UnionConstructor(l.clone(), kts.clone()))
+ }
+ _ => {
+ drop(v_borrow);
+ Ret::Expr(expr)
+ }
+ }
+ }
+ ExprF::ProjectionByExpr(_, _) => {
+ unimplemented!("selection by expression")
+ }
+
+ ExprF::Merge(ref handlers, ref variant, _) => {
+ let handlers_borrow = handlers.as_whnf();
+ let variant_borrow = variant.as_whnf();
+ match (&*handlers_borrow, &*variant_borrow) {
+ (RecordLit(kvs), UnionConstructor(l, _)) => match kvs.get(l) {
+ Some(h) => Ret::Value(h.clone()),
+ None => {
+ drop(handlers_borrow);
+ drop(variant_borrow);
+ Ret::Expr(expr)
+ }
+ },
+ (RecordLit(kvs), UnionLit(l, v, _)) => match kvs.get(l) {
+ Some(h) => Ret::Value(h.app(v.clone())),
+ None => {
+ drop(handlers_borrow);
+ drop(variant_borrow);
+ Ret::Expr(expr)
+ }
+ },
+ _ => {
+ drop(handlers_borrow);
+ drop(variant_borrow);
+ Ret::Expr(expr)
+ }
+ }
+ }
+ ExprF::ToMap(_, _) => unimplemented!("toMap"),
+ };
+
+ match ret {
+ Ret::ValueF(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),
+ }
+}
+
+/// Normalize a ValueF into WHNF
+pub(crate) fn normalize_whnf(v: ValueF, ty: &Value) -> ValueF {
+ 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()))
+ }
+ // 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
new file mode 100644
index 0000000..e277e54
--- /dev/null
+++ b/dhall/src/semantics/phase/parse.rs
@@ -0,0 +1,37 @@
+use std::fs::File;
+use std::io::Read;
+use std::path::Path;
+
+use crate::syntax::parse_expr;
+
+use crate::error::Error;
+use crate::phase::resolve::ImportRoot;
+use crate::phase::Parsed;
+
+pub(crate) fn parse_file(f: &Path) -> Result<Parsed, Error> {
+ let mut buffer = String::new();
+ File::open(f)?.read_to_string(&mut buffer)?;
+ let expr = parse_expr(&*buffer)?;
+ let root = ImportRoot::LocalDir(f.parent().unwrap().to_owned());
+ Ok(Parsed(expr, root))
+}
+
+pub(crate) fn parse_str(s: &str) -> Result<Parsed, Error> {
+ let expr = parse_expr(s)?;
+ let root = ImportRoot::LocalDir(std::env::current_dir()?);
+ Ok(Parsed(expr, root))
+}
+
+pub(crate) fn parse_binary(data: &[u8]) -> Result<Parsed, Error> {
+ let expr = crate::phase::binary::decode(data)?;
+ let root = ImportRoot::LocalDir(std::env::current_dir()?);
+ Ok(Parsed(expr, root))
+}
+
+pub(crate) fn parse_binary_file(f: &Path) -> Result<Parsed, Error> {
+ let mut buffer = Vec::new();
+ File::open(f)?.read_to_end(&mut buffer)?;
+ let expr = crate::phase::binary::decode(&buffer)?;
+ let root = ImportRoot::LocalDir(f.parent().unwrap().to_owned());
+ Ok(Parsed(expr, root))
+}
diff --git a/dhall/src/semantics/phase/resolve.rs b/dhall/src/semantics/phase/resolve.rs
new file mode 100644
index 0000000..5920f82
--- /dev/null
+++ b/dhall/src/semantics/phase/resolve.rs
@@ -0,0 +1,180 @@
+use std::collections::HashMap;
+use std::path::{Path, PathBuf};
+
+use crate::error::{Error, ImportError};
+use crate::phase::{Normalized, NormalizedExpr, Parsed, Resolved};
+use crate::syntax::{FilePath, ImportLocation, URL};
+
+type Import = crate::syntax::Import<NormalizedExpr>;
+
+/// A root from which to resolve relative imports.
+#[derive(Debug, Clone, PartialEq, Eq)]
+pub(crate) enum ImportRoot {
+ LocalDir(PathBuf),
+}
+
+type ImportCache = HashMap<Import, Normalized>;
+
+pub(crate) type ImportStack = Vec<Import>;
+
+fn resolve_import(
+ import: &Import,
+ root: &ImportRoot,
+ import_cache: &mut ImportCache,
+ import_stack: &ImportStack,
+) -> Result<Normalized, ImportError> {
+ use self::ImportRoot::*;
+ use crate::syntax::FilePrefix::*;
+ use crate::syntax::ImportLocation::*;
+ let cwd = match root {
+ LocalDir(cwd) => cwd,
+ };
+ match &import.location {
+ Local(prefix, path) => {
+ let path_buf: PathBuf = path.file_path.iter().collect();
+ let path_buf = match prefix {
+ // TODO: fail gracefully
+ Parent => cwd.parent().unwrap().join(path_buf),
+ Here => cwd.join(path_buf),
+ _ => unimplemented!("{:?}", import),
+ };
+ Ok(load_import(&path_buf, import_cache, import_stack).map_err(
+ |e| ImportError::Recursive(import.clone(), Box::new(e)),
+ )?)
+ }
+ _ => unimplemented!("{:?}", import),
+ }
+}
+
+fn load_import(
+ f: &Path,
+ import_cache: &mut ImportCache,
+ import_stack: &ImportStack,
+) -> Result<Normalized, Error> {
+ Ok(
+ do_resolve_expr(Parsed::parse_file(f)?, import_cache, import_stack)?
+ .typecheck()?
+ .normalize(),
+ )
+}
+
+fn do_resolve_expr(
+ parsed: Parsed,
+ import_cache: &mut ImportCache,
+ import_stack: &ImportStack,
+) -> Result<Resolved, ImportError> {
+ let Parsed(mut expr, root) = parsed;
+ let mut resolve = |import: Import| -> Result<Normalized, ImportError> {
+ if import_stack.contains(&import) {
+ return Err(ImportError::ImportCycle(import_stack.clone(), import));
+ }
+ match import_cache.get(&import) {
+ Some(expr) => Ok(expr.clone()),
+ None => {
+ // Copy the import stack and push the current import
+ let mut import_stack = import_stack.clone();
+ import_stack.push(import.clone());
+
+ // Resolve the import recursively
+ let expr = resolve_import(
+ &import,
+ &root,
+ import_cache,
+ &import_stack,
+ )?;
+
+ // Add the import to the cache
+ import_cache.insert(import, expr.clone());
+ Ok(expr)
+ }
+ }
+ };
+ expr.traverse_resolve_mut(&mut resolve)?;
+ Ok(Resolved(expr))
+}
+
+pub(crate) fn resolve(e: Parsed) -> Result<Resolved, ImportError> {
+ do_resolve_expr(e, &mut HashMap::new(), &Vec::new())
+}
+
+pub(crate) fn skip_resolve_expr(
+ parsed: Parsed,
+) -> Result<Resolved, ImportError> {
+ let mut expr = parsed.0;
+ let mut resolve = |import: Import| -> Result<Normalized, ImportError> {
+ Err(ImportError::UnexpectedImport(import))
+ };
+ expr.traverse_resolve_mut(&mut resolve)?;
+ Ok(Resolved(expr))
+}
+
+pub trait Canonicalize {
+ fn canonicalize(&self) -> Self;
+}
+
+impl Canonicalize for FilePath {
+ fn canonicalize(&self) -> FilePath {
+ let mut file_path = Vec::new();
+ let mut file_path_components = self.file_path.clone().into_iter();
+
+ loop {
+ let component = file_path_components.next();
+ match component.as_ref() {
+ // ───────────────────
+ // canonicalize(ε) = ε
+ None => break,
+
+ // canonicalize(directory₀) = directory₁
+ // ───────────────────────────────────────
+ // canonicalize(directory₀/.) = directory₁
+ Some(c) if c == "." => continue,
+
+ Some(c) if c == ".." => match file_path_components.next() {
+ // canonicalize(directory₀) = ε
+ // ────────────────────────────
+ // canonicalize(directory₀/..) = /..
+ None => file_path.push("..".to_string()),
+
+ // canonicalize(directory₀) = directory₁/..
+ // ──────────────────────────────────────────────
+ // canonicalize(directory₀/..) = directory₁/../..
+ Some(ref c) if c == ".." => {
+ file_path.push("..".to_string());
+ file_path.push("..".to_string());
+ }
+
+ // canonicalize(directory₀) = directory₁/component
+ // ─────────────────────────────────────────────── ; If "component" is not
+ // canonicalize(directory₀/..) = directory₁ ; ".."
+ Some(_) => continue,
+ },
+
+ // canonicalize(directory₀) = directory₁
+ // ───────────────────────────────────────────────────────── ; If no other
+ // canonicalize(directory₀/component) = directory₁/component ; rule matches
+ Some(c) => file_path.push(c.clone()),
+ }
+ }
+
+ FilePath { file_path }
+ }
+}
+
+impl<SE: Copy> Canonicalize for ImportLocation<SE> {
+ fn canonicalize(&self) -> ImportLocation<SE> {
+ match self {
+ ImportLocation::Local(prefix, file) => {
+ ImportLocation::Local(*prefix, file.canonicalize())
+ }
+ ImportLocation::Remote(url) => ImportLocation::Remote(URL {
+ scheme: url.scheme,
+ authority: url.authority.clone(),
+ path: url.path.canonicalize(),
+ query: url.query.clone(),
+ headers: url.headers.clone(),
+ }),
+ ImportLocation::Env(name) => ImportLocation::Env(name.to_string()),
+ ImportLocation::Missing => ImportLocation::Missing,
+ }
+ }
+}
diff --git a/dhall/src/semantics/phase/typecheck.rs b/dhall/src/semantics/phase/typecheck.rs
new file mode 100644
index 0000000..9a41be9
--- /dev/null
+++ b/dhall/src/semantics/phase/typecheck.rs
@@ -0,0 +1,815 @@
+use std::cmp::max;
+use std::collections::HashMap;
+
+use crate::syntax::{
+ Builtin, Const, Expr, ExprF, InterpolatedTextContents, Label, RawExpr, Span,
+};
+
+use crate::core::context::TypecheckContext;
+use crate::core::value::Value;
+use crate::core::valuef::ValueF;
+use crate::core::var::{Shift, Subst};
+use crate::error::{TypeError, TypeMessage};
+use crate::phase::Normalized;
+
+fn tck_pi_type(
+ ctx: &TypecheckContext,
+ x: Label,
+ tx: Value,
+ te: Value,
+) -> Result<Value, TypeError> {
+ use crate::error::TypeMessage::*;
+ let ctx2 = ctx.insert_type(&x, tx.clone());
+
+ let ka = match tx.get_type()?.as_const() {
+ Some(k) => k,
+ _ => return Err(TypeError::new(ctx, InvalidInputType(tx))),
+ };
+
+ let kb = match te.get_type()?.as_const() {
+ Some(k) => k,
+ _ => {
+ return Err(TypeError::new(
+ &ctx2,
+ InvalidOutputType(te.get_type()?),
+ ))
+ }
+ };
+
+ let k = function_check(ka, kb);
+
+ Ok(Value::from_valuef_and_type(
+ ValueF::Pi(x.into(), tx, te),
+ Value::from_const(k),
+ ))
+}
+
+fn tck_record_type(
+ ctx: &TypecheckContext,
+ kts: impl IntoIterator<Item = Result<(Label, Value), TypeError>>,
+) -> Result<Value, TypeError> {
+ use crate::error::TypeMessage::*;
+ use std::collections::hash_map::Entry;
+ let mut new_kts = HashMap::new();
+ // An empty record type has type Type
+ let mut k = Const::Type;
+ for e in kts {
+ let (x, t) = e?;
+ // Construct the union of the contained `Const`s
+ match t.get_type()?.as_const() {
+ Some(k2) => k = max(k, k2),
+ None => return Err(TypeError::new(ctx, InvalidFieldType(x, t))),
+ }
+ // Check for duplicated entries
+ let entry = new_kts.entry(x);
+ match &entry {
+ Entry::Occupied(_) => {
+ return Err(TypeError::new(ctx, RecordTypeDuplicateField))
+ }
+ Entry::Vacant(_) => entry.or_insert_with(|| t),
+ };
+ }
+
+ Ok(Value::from_valuef_and_type(
+ ValueF::RecordType(new_kts),
+ Value::from_const(k),
+ ))
+}
+
+fn tck_union_type<Iter>(
+ ctx: &TypecheckContext,
+ kts: Iter,
+) -> Result<Value, TypeError>
+where
+ Iter: IntoIterator<Item = Result<(Label, Option<Value>), TypeError>>,
+{
+ use crate::error::TypeMessage::*;
+ use std::collections::hash_map::Entry;
+ let mut new_kts = HashMap::new();
+ // Check that all types are the same const
+ let mut k = None;
+ for e in kts {
+ let (x, t) = e?;
+ if let Some(t) = &t {
+ match (k, t.get_type()?.as_const()) {
+ (None, Some(k2)) => k = Some(k2),
+ (Some(k1), Some(k2)) if k1 == k2 => {}
+ _ => {
+ return Err(TypeError::new(
+ ctx,
+ InvalidFieldType(x, t.clone()),
+ ))
+ }
+ }
+ }
+ let entry = new_kts.entry(x);
+ match &entry {
+ Entry::Occupied(_) => {
+ return Err(TypeError::new(ctx, UnionTypeDuplicateField))
+ }
+ Entry::Vacant(_) => entry.or_insert_with(|| t),
+ };
+ }
+
+ // An empty union type has type Type;
+ // 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),
+ Value::from_const(k),
+ ))
+}
+
+fn function_check(a: Const, b: Const) -> Const {
+ if b == Const::Type {
+ Const::Type
+ } else {
+ max(a, b)
+ }
+}
+
+pub(crate) fn const_to_value(c: Const) -> Value {
+ let v = ValueF::Const(c);
+ match c {
+ Const::Type => {
+ Value::from_valuef_and_type(v, const_to_value(Const::Kind))
+ }
+ Const::Kind => {
+ Value::from_valuef_and_type(v, const_to_value(Const::Sort))
+ }
+ Const::Sort => Value::const_sort(),
+ }
+}
+
+pub fn rc<E>(x: RawExpr<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) };
+ ($var:ident) => {
+ ExprF::Var(crate::syntax::V(stringify!($var).into(), 0))
+ };
+ (Optional $ty:ident) => {
+ ExprF::App(
+ rc(ExprF::Builtin(Builtin::Optional)),
+ rc(make_type!($ty))
+ )
+ };
+ (List $($rest:tt)*) => {
+ ExprF::App(
+ rc(ExprF::Builtin(Builtin::List)),
+ rc(make_type!($($rest)*))
+ )
+ };
+ ({ $($label:ident : $ty:ident),* }) => {{
+ let mut kts = crate::syntax::map::DupTreeMap::new();
+ $(
+ kts.insert(
+ Label::from(stringify!($label)),
+ rc(make_type!($ty)),
+ );
+ )*
+ ExprF::RecordType(kts)
+ }};
+ ($ty:ident -> $($rest:tt)*) => {
+ ExprF::Pi(
+ "_".into(),
+ rc(make_type!($ty)),
+ rc(make_type!($($rest)*))
+ )
+ };
+ (($($arg:tt)*) -> $($rest:tt)*) => {
+ ExprF::Pi(
+ "_".into(),
+ rc(make_type!($($arg)*)),
+ rc(make_type!($($rest)*))
+ )
+ };
+ (forall ($var:ident : $($ty:tt)*) -> $($rest:tt)*) => {
+ ExprF::Pi(
+ stringify!($var).into(),
+ rc(make_type!($($ty)*)),
+ rc(make_type!($($rest)*))
+ )
+ };
+}
+
+fn type_of_builtin<E>(b: Builtin) -> Expr<E> {
+ use crate::syntax::Builtin::*;
+ rc(match b {
+ Bool | Natural | Integer | Double | Text => make_type!(Type),
+ List | Optional => make_type!(
+ Type -> Type
+ ),
+
+ NaturalFold => make_type!(
+ Natural ->
+ forall (natural: Type) ->
+ forall (succ: natural -> natural) ->
+ forall (zero: natural) ->
+ natural
+ ),
+ NaturalBuild => make_type!(
+ (forall (natural: Type) ->
+ forall (succ: natural -> natural) ->
+ forall (zero: natural) ->
+ natural) ->
+ Natural
+ ),
+ NaturalIsZero | NaturalEven | NaturalOdd => make_type!(
+ Natural -> Bool
+ ),
+ NaturalToInteger => make_type!(Natural -> Integer),
+ NaturalShow => make_type!(Natural -> Text),
+ NaturalSubtract => make_type!(Natural -> Natural -> Natural),
+
+ IntegerToDouble => make_type!(Integer -> Double),
+ IntegerShow => make_type!(Integer -> Text),
+ DoubleShow => make_type!(Double -> Text),
+ TextShow => make_type!(Text -> Text),
+
+ ListBuild => make_type!(
+ forall (a: Type) ->
+ (forall (list: Type) ->
+ forall (cons: a -> list -> list) ->
+ forall (nil: list) ->
+ list) ->
+ List a
+ ),
+ ListFold => make_type!(
+ forall (a: Type) ->
+ (List a) ->
+ forall (list: Type) ->
+ forall (cons: a -> list -> list) ->
+ forall (nil: list) ->
+ list
+ ),
+ ListLength => make_type!(forall (a: Type) -> (List a) -> Natural),
+ ListHead | ListLast => {
+ make_type!(forall (a: Type) -> (List a) -> Optional a)
+ }
+ ListIndexed => make_type!(
+ forall (a: Type) ->
+ (List a) ->
+ List { index: Natural, value: a }
+ ),
+ ListReverse => make_type!(
+ forall (a: Type) -> (List a) -> List a
+ ),
+
+ OptionalBuild => make_type!(
+ forall (a: Type) ->
+ (forall (optional: Type) ->
+ forall (just: a -> optional) ->
+ forall (nothing: optional) ->
+ optional) ->
+ Optional a
+ ),
+ OptionalFold => make_type!(
+ forall (a: Type) ->
+ (Optional a) ->
+ forall (optional: Type) ->
+ forall (just: a -> optional) ->
+ forall (nothing: optional) ->
+ optional
+ ),
+ OptionalNone => make_type!(
+ forall (a: Type) -> Optional a
+ ),
+ })
+}
+
+pub(crate) fn builtin_to_value(b: Builtin) -> Value {
+ let ctx = TypecheckContext::new();
+ Value::from_valuef_and_type(
+ ValueF::from_builtin(b),
+ type_with(&ctx, type_of_builtin(b)).unwrap(),
+ )
+}
+
+/// Type-check an expression and return the expression alongside its type if type-checking
+/// succeeded, or an error if type-checking failed.
+/// Some normalization is done while typechecking, so the returned expression might be partially
+/// normalized as well.
+fn type_with(
+ ctx: &TypecheckContext,
+ e: Expr<Normalized>,
+) -> Result<Value, TypeError> {
+ use crate::syntax::ExprF::{Annot, Embed, Lam, Let, Pi, Var};
+ let span = e.span();
+
+ Ok(match e.as_ref() {
+ Lam(var, annot, body) => {
+ let annot = type_with(ctx, annot.clone())?;
+ 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),
+ tck_pi_type(ctx, var.clone(), annot, body_type)?,
+ )
+ }
+ Pi(x, ta, tb) => {
+ let ta = type_with(ctx, ta.clone())?;
+ let ctx2 = ctx.insert_type(x, ta.clone());
+ let tb = type_with(&ctx2, tb.clone())?;
+ return tck_pi_type(ctx, x.clone(), ta, tb);
+ }
+ Let(x, t, v, e) => {
+ let v = if let Some(t) = t {
+ t.rewrap(Annot(v.clone(), t.clone()))
+ } else {
+ v.clone()
+ };
+
+ let v = type_with(ctx, v)?;
+ return type_with(&ctx.insert_value(x, v.clone())?, e.clone());
+ }
+ Embed(p) => p.clone().into_typed().into_value(),
+ Var(var) => match ctx.lookup(&var) {
+ Some(typed) => typed.clone(),
+ None => {
+ return Err(TypeError::new(
+ ctx,
+ TypeMessage::UnboundVariable(span),
+ ))
+ }
+ },
+ e => {
+ // Typecheck recursively all subexpressions
+ let expr = e.traverse_ref_with_special_handling_of_binders(
+ |e| type_with(ctx, e.clone()),
+ |_, _| unreachable!(),
+ )?;
+ type_last_layer(ctx, expr, span)?
+ }
+ })
+}
+
+/// When all sub-expressions have been typed, check the remaining toplevel
+/// layer.
+fn type_last_layer(
+ ctx: &TypecheckContext,
+ e: ExprF<Value, Normalized>,
+ span: Span,
+) -> Result<Value, TypeError> {
+ use crate::error::TypeMessage::*;
+ use crate::syntax::BinOp::*;
+ use crate::syntax::Builtin::*;
+ use crate::syntax::Const::Type;
+ use crate::syntax::ExprF::*;
+ let mkerr = |msg: TypeMessage| Err(TypeError::new(ctx, msg));
+
+ /// Intermediary return type
+ enum Ret {
+ /// Returns the contained value as is
+ RetWhole(Value),
+ /// Returns the input expression `e` with the contained value as its type
+ RetTypeOnly(Value),
+ }
+ use Ret::*;
+
+ let ret = match &e {
+ Import(_) => unreachable!(
+ "There should remain no imports in a resolved expression"
+ ),
+ Lam(_, _, _) | Pi(_, _, _) | Let(_, _, _, _) | Embed(_) | Var(_) => {
+ unreachable!()
+ }
+ App(f, a) => {
+ 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),
+ _ => return mkerr(NotAFunction(f.clone())),
+ };
+ if &a.get_type()? != tx {
+ return mkerr(TypeMismatch(f.clone(), tx.clone(), a.clone()));
+ }
+
+ RetTypeOnly(tb.subst_shift(&x.into(), a))
+ }
+ Annot(x, t) => {
+ if &x.get_type()? != t {
+ return mkerr(AnnotMismatch(x.clone(), t.clone()));
+ }
+ RetWhole(x.clone())
+ }
+ Assert(t) => {
+ match &*t.as_whnf() {
+ ValueF::Equivalence(x, y) if x == y => {}
+ ValueF::Equivalence(x, y) => {
+ return mkerr(AssertMismatch(x.clone(), y.clone()))
+ }
+ _ => return mkerr(AssertMustTakeEquivalence),
+ }
+ RetTypeOnly(t.clone())
+ }
+ BoolIf(x, y, z) => {
+ if *x.get_type()?.as_whnf() != ValueF::from_builtin(Bool) {
+ return mkerr(InvalidPredicate(x.clone()));
+ }
+
+ if y.get_type()?.get_type()?.as_const() != Some(Type) {
+ return mkerr(IfBranchMustBeTerm(true, y.clone()));
+ }
+
+ if z.get_type()?.get_type()?.as_const() != Some(Type) {
+ return mkerr(IfBranchMustBeTerm(false, z.clone()));
+ }
+
+ if y.get_type()? != z.get_type()? {
+ return mkerr(IfBranchMismatch(y.clone(), z.clone()));
+ }
+
+ RetTypeOnly(y.get_type()?)
+ }
+ EmptyListLit(t) => {
+ match &*t.as_whnf() {
+ ValueF::AppliedBuiltin(crate::syntax::Builtin::List, args)
+ if args.len() == 1 => {}
+ _ => return mkerr(InvalidListType(t.clone())),
+ }
+ RetTypeOnly(t.clone())
+ }
+ NEListLit(xs) => {
+ let mut iter = xs.iter().enumerate();
+ let (_, x) = iter.next().unwrap();
+ for (i, y) in iter {
+ if x.get_type()? != y.get_type()? {
+ return mkerr(InvalidListElement(
+ i,
+ x.get_type()?,
+ y.clone(),
+ ));
+ }
+ }
+ let t = x.get_type()?;
+ if t.get_type()?.as_const() != Some(Type) {
+ return mkerr(InvalidListType(t));
+ }
+
+ RetTypeOnly(Value::from_builtin(crate::syntax::Builtin::List).app(t))
+ }
+ SomeLit(x) => {
+ let t = x.get_type()?;
+ if t.get_type()?.as_const() != Some(Type) {
+ return mkerr(InvalidOptionalType(t));
+ }
+
+ RetTypeOnly(
+ Value::from_builtin(crate::syntax::Builtin::Optional).app(t),
+ )
+ }
+ RecordType(kts) => RetWhole(tck_record_type(
+ ctx,
+ kts.iter().map(|(x, t)| Ok((x.clone(), t.clone()))),
+ )?),
+ UnionType(kts) => RetWhole(tck_union_type(
+ ctx,
+ kts.iter().map(|(x, t)| Ok((x.clone(), t.clone()))),
+ )?),
+ RecordLit(kvs) => RetTypeOnly(tck_record_type(
+ ctx,
+ kvs.iter().map(|(x, v)| Ok((x.clone(), v.get_type()?))),
+ )?),
+ Field(r, x) => {
+ match &*r.get_type()?.as_whnf() {
+ ValueF::RecordType(kts) => match kts.get(&x) {
+ Some(tth) => {
+ RetTypeOnly(tth.clone())
+ },
+ None => return mkerr(MissingRecordField(x.clone(),
+ r.clone())),
+ },
+ // TODO: branch here only when r.get_type() is a Const
+ _ => {
+ match &*r.as_whnf() {
+ ValueF::UnionType(kts) => match kts.get(&x) {
+ // Constructor has type T -> < x: T, ... >
+ Some(Some(t)) => {
+ RetTypeOnly(
+ tck_pi_type(
+ ctx,
+ "_".into(),
+ t.clone(),
+ r.under_binder(Label::from("_")),
+ )?
+ )
+ },
+ Some(None) => {
+ RetTypeOnly(r.clone())
+ },
+ None => {
+ return mkerr(MissingUnionField(
+ x.clone(),
+ r.clone(),
+ ))
+ },
+ },
+ _ => {
+ return mkerr(NotARecord(
+ x.clone(),
+ r.clone()
+ ))
+ },
+ }
+ }
+ // _ => mkerr(NotARecord(
+ // x,
+ // r?,
+ // )),
+ }
+ }
+ Const(c) => RetWhole(const_to_value(*c)),
+ Builtin(b) => RetWhole(builtin_to_value(*b)),
+ BoolLit(_) => RetTypeOnly(builtin_to_value(Bool)),
+ NaturalLit(_) => RetTypeOnly(builtin_to_value(Natural)),
+ IntegerLit(_) => RetTypeOnly(builtin_to_value(Integer)),
+ DoubleLit(_) => RetTypeOnly(builtin_to_value(Double)),
+ TextLit(interpolated) => {
+ let text_type = builtin_to_value(Text);
+ for contents in interpolated.iter() {
+ use InterpolatedTextContents::Expr;
+ if let Expr(x) = contents {
+ if x.get_type()? != text_type {
+ return mkerr(InvalidTextInterpolation(x.clone()));
+ }
+ }
+ }
+ RetTypeOnly(text_type)
+ }
+ BinOp(RightBiasedRecordMerge, l, r) => {
+ use crate::phase::normalize::merge_maps;
+
+ let l_type = l.get_type()?;
+ let r_type = r.get_type()?;
+
+ // Extract the LHS record type
+ let l_type_borrow = l_type.as_whnf();
+ let kts_x = match &*l_type_borrow {
+ ValueF::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,
+ _ => return mkerr(MustCombineRecord(r.clone())),
+ };
+
+ // Union the two records, prefering
+ // the values found in the RHS.
+ let kts = merge_maps::<_, _, _, !>(kts_x, kts_y, |_, _, r_t| {
+ Ok(r_t.clone())
+ })?;
+
+ // Construct the final record type from the union
+ RetTypeOnly(tck_record_type(
+ ctx,
+ kts.into_iter().map(|(x, v)| Ok((x.clone(), v))),
+ )?)
+ }
+ BinOp(RecursiveRecordMerge, l, r) => RetTypeOnly(type_last_layer(
+ ctx,
+ ExprF::BinOp(
+ RecursiveRecordTypeMerge,
+ l.get_type()?,
+ r.get_type()?,
+ ),
+ Span::Artificial,
+ )?),
+ BinOp(RecursiveRecordTypeMerge, l, r) => {
+ use crate::phase::normalize::merge_maps;
+
+ // Extract the LHS record type
+ let borrow_l = l.as_whnf();
+ let kts_x = match &*borrow_l {
+ ValueF::RecordType(kts) => kts,
+ _ => {
+ return mkerr(RecordTypeMergeRequiresRecordType(l.clone()))
+ }
+ };
+
+ // Extract the RHS record type
+ let borrow_r = r.as_whnf();
+ let kts_y = match &*borrow_r {
+ ValueF::RecordType(kts) => kts,
+ _ => {
+ return mkerr(RecordTypeMergeRequiresRecordType(r.clone()))
+ }
+ };
+
+ // Ensure that the records combine without a type error
+ let kts = merge_maps(
+ kts_x,
+ kts_y,
+ // If the Label exists for both records, then we hit the recursive case.
+ |_, l: &Value, r: &Value| {
+ type_last_layer(
+ ctx,
+ ExprF::BinOp(
+ RecursiveRecordTypeMerge,
+ l.clone(),
+ r.clone(),
+ ),
+ Span::Artificial,
+ )
+ },
+ )?;
+
+ RetWhole(tck_record_type(ctx, kts.into_iter().map(Ok))?)
+ }
+ BinOp(o @ ListAppend, l, r) => {
+ match &*l.get_type()?.as_whnf() {
+ ValueF::AppliedBuiltin(List, _) => {}
+ _ => return mkerr(BinOpTypeMismatch(*o, l.clone())),
+ }
+
+ if l.get_type()? != r.get_type()? {
+ return mkerr(BinOpTypeMismatch(*o, r.clone()));
+ }
+
+ RetTypeOnly(l.get_type()?)
+ }
+ BinOp(Equivalence, l, r) => {
+ if l.get_type()?.get_type()?.as_const() != Some(Type) {
+ return mkerr(EquivalenceArgumentMustBeTerm(true, l.clone()));
+ }
+ if r.get_type()?.get_type()?.as_const() != Some(Type) {
+ return mkerr(EquivalenceArgumentMustBeTerm(false, r.clone()));
+ }
+
+ if l.get_type()? != r.get_type()? {
+ return mkerr(EquivalenceTypeMismatch(r.clone(), l.clone()));
+ }
+
+ RetWhole(Value::from_valuef_and_type(
+ ValueF::Equivalence(l.clone(), r.clone()),
+ Value::from_const(Type),
+ ))
+ }
+ BinOp(o, l, r) => {
+ let t = builtin_to_value(match o {
+ BoolAnd => Bool,
+ BoolOr => Bool,
+ BoolEQ => Bool,
+ BoolNE => Bool,
+ NaturalPlus => Natural,
+ NaturalTimes => Natural,
+ TextAppend => Text,
+ ListAppend => unreachable!(),
+ RightBiasedRecordMerge => unreachable!(),
+ RecursiveRecordMerge => unreachable!(),
+ RecursiveRecordTypeMerge => unreachable!(),
+ ImportAlt => unreachable!("There should remain no import alternatives in a resolved expression"),
+ Equivalence => unreachable!(),
+ });
+
+ if l.get_type()? != t {
+ return mkerr(BinOpTypeMismatch(*o, l.clone()));
+ }
+
+ if r.get_type()? != t {
+ return mkerr(BinOpTypeMismatch(*o, r.clone()));
+ }
+
+ RetTypeOnly(t)
+ }
+ Merge(record, union, type_annot) => {
+ let record_type = record.get_type()?;
+ let record_borrow = record_type.as_whnf();
+ let handlers = match &*record_borrow {
+ ValueF::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,
+ _ => return mkerr(Merge2ArgMustBeUnion(union.clone())),
+ };
+
+ let mut inferred_type = None;
+ for (x, handler_type) in handlers {
+ let handler_return_type =
+ match variants.get(x) {
+ // Union alternative with type
+ 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),
+ _ => {
+ return mkerr(NotAFunction(
+ handler_type.clone(),
+ ))
+ }
+ };
+
+ if variant_type != tx {
+ return mkerr(TypeMismatch(
+ handler_type.clone(),
+ tx.clone(),
+ variant_type.clone(),
+ ));
+ }
+
+ // Extract `tb` from under the `x` binder. Fails is `x` was free in `tb`.
+ match tb.over_binder(x) {
+ Some(x) => x,
+ None => return mkerr(
+ MergeHandlerReturnTypeMustNotBeDependent,
+ ),
+ }
+ }
+ // Union alternative without type
+ Some(None) => handler_type.clone(),
+ None => {
+ return mkerr(MergeHandlerMissingVariant(x.clone()))
+ }
+ };
+ match &inferred_type {
+ None => inferred_type = Some(handler_return_type),
+ Some(t) => {
+ if t != &handler_return_type {
+ return mkerr(MergeHandlerTypeMismatch);
+ }
+ }
+ }
+ }
+ for x in variants.keys() {
+ if !handlers.contains_key(x) {
+ return mkerr(MergeVariantMissingHandler(x.clone()));
+ }
+ }
+
+ match (inferred_type, type_annot) {
+ (Some(ref t1), Some(t2)) => {
+ if t1 != t2 {
+ return mkerr(MergeAnnotMismatch);
+ }
+ RetTypeOnly(t2.clone())
+ }
+ (Some(t), None) => RetTypeOnly(t),
+ (None, Some(t)) => RetTypeOnly(t.clone()),
+ (None, None) => return mkerr(MergeEmptyNeedsAnnotation),
+ }
+ }
+ ToMap(_, _) => unimplemented!("toMap"),
+ Projection(record, labels) => {
+ let record_type = record.get_type()?;
+ let record_type_borrow = record_type.as_whnf();
+ let kts = match &*record_type_borrow {
+ ValueF::RecordType(kts) => kts,
+ _ => return mkerr(ProjectionMustBeRecord),
+ };
+
+ let mut new_kts = HashMap::new();
+ for l in labels {
+ match kts.get(l) {
+ None => return mkerr(ProjectionMissingEntry),
+ Some(t) => new_kts.insert(l.clone(), t.clone()),
+ };
+ }
+
+ RetTypeOnly(Value::from_valuef_and_type(
+ ValueF::RecordType(new_kts),
+ record_type.get_type()?,
+ ))
+ }
+ ProjectionByExpr(_, _) => unimplemented!("selection by expression"),
+ };
+
+ Ok(match ret {
+ RetTypeOnly(typ) => Value::from_valuef_and_type_and_span(
+ ValueF::PartialExpr(e),
+ typ,
+ span,
+ ),
+ RetWhole(v) => v.with_span(span),
+ })
+}
+
+/// `type_of` is the same as `type_with` with an empty context, meaning that the
+/// expression must be closed (i.e. no free variables), otherwise type-checking
+/// will fail.
+pub(crate) fn typecheck(e: Expr<Normalized>) -> Result<Value, TypeError> {
+ type_with(&TypecheckContext::new(), e)
+}
+
+pub(crate) fn typecheck_with(
+ expr: Expr<Normalized>,
+ ty: Expr<Normalized>,
+) -> Result<Value, TypeError> {
+ typecheck(expr.rewrap(ExprF::Annot(expr.clone(), ty)))
+}
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-05 18:34:36 +0000