diff options
author | Nadrieril | 2019-11-11 11:34:29 +0000 |
---|---|---|
committer | Nadrieril | 2019-11-11 13:50:36 +0000 |
commit | 5d5a356b8eb36e277c312e5550d1cb0a2f82e9fa (patch) | |
tree | babaa2061bd48769006973ee74073f61b0ac3f5e /dhall/src/core | |
parent | b68c3af578d1f6b0d1e32e7d88ef57774fb468d8 (diff) |
Store a `Span` in `Value`
Diffstat (limited to 'dhall/src/core')
-rw-r--r-- | dhall/src/core/value.rs | 23 |
1 files changed, 19 insertions, 4 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(), } } } |