summaryrefslogtreecommitdiff
path: root/dhall/src
diff options
context:
space:
mode:
Diffstat (limited to 'dhall/src')
-rw-r--r--dhall/src/core/value.rs23
-rw-r--r--dhall/src/phase/typecheck.rs14
2 files changed, 29 insertions, 8 deletions
diff --git a/dhall/src/core/value.rs b/dhall/src/core/value.rs
index b4b6b08..b6c156e 100644
--- a/dhall/src/core/value.rs
+++ b/dhall/src/core/value.rs
@@ -1,7 +1,7 @@
use std::cell::{Ref, RefCell, RefMut};
use std::rc::Rc;
-use dhall_syntax::{Builtin, Const};
+use dhall_syntax::{Builtin, Const, Span};
use crate::core::context::TypecheckContext;
use crate::core::valuef::ValueF;
@@ -36,6 +36,7 @@ struct ValueInternal {
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,
@@ -69,18 +70,21 @@ impl 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,
@@ -113,11 +117,12 @@ impl ValueInternal {
}
impl Value {
- fn new(value: ValueF, form: Form, ty: Value) -> Value {
+ fn new(value: ValueF, form: Form, ty: Value, span: Span) -> Value {
ValueInternal {
form,
value,
ty: Some(ty),
+ span,
}
.into_value()
}
@@ -126,14 +131,22 @@ impl Value {
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)
+ Value::new(v, Unevaled, t, Span::PlaceHolder)
+ }
+ 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)
+ Value::new(v, WHNF, t, Span::PlaceHolder)
}
pub(crate) fn from_const(c: Const) -> Self {
const_to_value(c)
@@ -258,6 +271,7 @@ impl Shift for ValueInternal {
form: self.form,
value: self.value.shift(delta, var)?,
ty: self.ty.shift(delta, var)?,
+ span: self.span.clone(),
})
}
}
@@ -285,6 +299,7 @@ impl Subst<Value> for ValueInternal {
form: Unevaled,
value: self.value.subst_shift(var, val),
ty: self.ty.subst_shift(var, val),
+ span: self.span.clone(),
}
}
}
diff --git a/dhall/src/phase/typecheck.rs b/dhall/src/phase/typecheck.rs
index 4d8c7d3..63f5157 100644
--- a/dhall/src/phase/typecheck.rs
+++ b/dhall/src/phase/typecheck.rs
@@ -304,6 +304,7 @@ fn type_with(
e: Expr<Normalized>,
) -> Result<Value, TypeError> {
use dhall_syntax::ExprF::{Annot, Embed, Lam, Let, Pi, Var};
+ let span = e.span();
Ok(match e.as_ref() {
Lam(var, annot, body) => {
@@ -348,7 +349,7 @@ fn type_with(
|e| type_with(ctx, e.clone()),
|_, _| unreachable!(),
)?;
- type_last_layer(ctx, expr)?
+ type_last_layer(ctx, expr, span)?
}
})
}
@@ -358,6 +359,7 @@ fn type_with(
fn type_last_layer(
ctx: &TypecheckContext,
e: ExprF<Value, Normalized>,
+ span: Span,
) -> Result<Value, TypeError> {
use crate::error::TypeMessage::*;
use dhall_syntax::BinOp::*;
@@ -584,6 +586,7 @@ fn type_last_layer(
l.get_type()?,
r.get_type()?,
),
+ Span::PlaceHolder,
)?),
BinOp(RecursiveRecordTypeMerge, l, r) => {
use crate::phase::normalize::merge_maps;
@@ -619,6 +622,7 @@ fn type_last_layer(
l.clone(),
r.clone(),
),
+ Span::PlaceHolder,
)
},
)?;
@@ -786,9 +790,11 @@ fn type_last_layer(
};
Ok(match ret {
- RetTypeOnly(typ) => {
- Value::from_valuef_and_type(ValueF::PartialExpr(e), typ)
- }
+ RetTypeOnly(typ) => Value::from_valuef_and_type_and_span(
+ ValueF::PartialExpr(e),
+ typ,
+ span,
+ ),
RetWhole(v) => v,
})
}