diff options
Diffstat (limited to '')
| -rw-r--r-- | dhall/src/semantics/core/value.rs | 162 |
1 files changed, 81 insertions, 81 deletions
diff --git a/dhall/src/semantics/core/value.rs b/dhall/src/semantics/core/value.rs index 9511cc2..1e3b965 100644 --- a/dhall/src/semantics/core/value.rs +++ b/dhall/src/semantics/core/value.rs @@ -11,6 +11,25 @@ use crate::semantics::phase::{NormalizedExpr, Typed}; use crate::semantics::to_expr; use crate::syntax::{Builtin, Const, Span}; +use self::Form::{Unevaled, NF, WHNF}; + +/// Stores a possibly unevaluated value. Gets (partially) normalized on-demand, +/// sharing computation automatically. Uses a RefCell to share computation. +/// Can optionally store a type from typechecking to preserve type information. +#[derive(Clone)] +pub(crate) struct Value(Rc<RefCell<ValueInternal>>); + +/// Invariant: if `form` is `WHNF`, `value` must be in Weak Head Normal Form +/// Invariant: if `form` is `NF`, `value` must be fully normalized +#[derive(Debug)] +struct ValueInternal { + form: Form, + kind: ValueKind, + /// This is None if and only if `value` is `Sort` (which doesn't have a type) + ty: Option<Value>, + span: Span, +} + #[derive(Debug, Clone, Copy)] pub(crate) enum Form { /// No constraints; expression may not be normalized at all. @@ -25,87 +44,6 @@ pub(crate) enum Form { /// if we have the first constructor of the NF at all levels, we actually have the NF. NF, } -use Form::{Unevaled, NF, WHNF}; - -/// Partially normalized value. -/// Invariant: if `form` is `WHNF`, `value` must be in Weak Head Normal Form -/// Invariant: if `form` is `NF`, `value` must be fully normalized -#[derive(Debug)] -struct ValueInternal { - form: Form, - kind: ValueKind, - /// This is None if and only if `value` is `Sort` (which doesn't have a type) - ty: Option<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>>); - -impl ValueInternal { - fn into_value(self) -> Value { - Value(Rc::new(RefCell::new(self))) - } - fn as_kind(&self) -> &ValueKind { - &self.kind - } - - fn normalize_whnf(&mut self) { - take_mut::take_or_recover( - self, - // Dummy value in case the other closure panics - || ValueInternal { - form: Unevaled, - kind: ValueKind::Const(Const::Type), - ty: None, - span: Span::Artificial, - }, - |vint| match (&vint.form, &vint.ty) { - (Unevaled, Some(ty)) => ValueInternal { - form: WHNF, - kind: normalize_whnf(vint.kind, &ty), - ty: vint.ty, - span: vint.span, - }, - // `value` is `Sort` - (Unevaled, None) => ValueInternal { - form: NF, - kind: ValueKind::Const(Const::Sort), - ty: None, - span: vint.span, - }, - // Already in WHNF - (WHNF, _) | (NF, _) => vint, - }, - ) - } - fn normalize_nf(&mut self) { - match self.form { - Unevaled => { - self.normalize_whnf(); - self.normalize_nf(); - } - WHNF => { - self.kind.normalize_mut(); - self.form = NF; - } - // Already in NF - NF => {} - } - } - - fn get_type(&self) -> Result<&Value, TypeError> { - match &self.ty { - Some(t) => Ok(t), - None => { - Err(TypeError::new(&TypecheckContext::new(), TypeMessage::Sort)) - } - } - } -} impl Value { fn new(kind: ValueKind, form: Form, ty: Value, span: Span) -> Value { @@ -258,6 +196,68 @@ impl Value { } } +impl ValueInternal { + fn into_value(self) -> Value { + Value(Rc::new(RefCell::new(self))) + } + fn as_kind(&self) -> &ValueKind { + &self.kind + } + + fn normalize_whnf(&mut self) { + take_mut::take_or_recover( + self, + // Dummy value in case the other closure panics + || ValueInternal { + form: Unevaled, + kind: ValueKind::Const(Const::Type), + ty: None, + span: Span::Artificial, + }, + |vint| match (&vint.form, &vint.ty) { + (Unevaled, Some(ty)) => ValueInternal { + form: WHNF, + kind: normalize_whnf(vint.kind, &ty), + ty: vint.ty, + span: vint.span, + }, + // `value` is `Sort` + (Unevaled, None) => ValueInternal { + form: NF, + kind: ValueKind::Const(Const::Sort), + ty: None, + span: vint.span, + }, + // Already in WHNF + (WHNF, _) | (NF, _) => vint, + }, + ) + } + fn normalize_nf(&mut self) { + match self.form { + Unevaled => { + self.normalize_whnf(); + self.normalize_nf(); + } + WHNF => { + self.kind.normalize_mut(); + self.form = NF; + } + // Already in NF + NF => {} + } + } + + fn get_type(&self) -> Result<&Value, TypeError> { + match &self.ty { + Some(t) => Ok(t), + None => { + Err(TypeError::new(&TypecheckContext::new(), TypeMessage::Sort)) + } + } + } +} + impl Shift for Value { fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> { Some(Value(self.0.shift(delta, var)?)) |