summaryrefslogtreecommitdiff
path: root/dhall/src/core
diff options
context:
space:
mode:
Diffstat (limited to 'dhall/src/core')
-rw-r--r--dhall/src/core/context.rs34
-rw-r--r--dhall/src/core/value.rs68
-rw-r--r--dhall/src/core/valuef.rs14
3 files changed, 51 insertions, 65 deletions
diff --git a/dhall/src/core/context.rs b/dhall/src/core/context.rs
index 851e4c4..deabe44 100644
--- a/dhall/src/core/context.rs
+++ b/dhall/src/core/context.rs
@@ -3,7 +3,7 @@ use std::rc::Rc;
use dhall_syntax::{Label, V};
-use crate::core::value::{TypedValue, Value};
+use crate::core::value::TypedValue;
use crate::core::valuef::ValueF;
use crate::core::var::{AlphaVar, Shift, Subst};
use crate::error::TypeError;
@@ -11,7 +11,7 @@ use crate::error::TypeError;
#[derive(Debug, Clone)]
enum CtxItem {
Kept(AlphaVar, TypedValue),
- Replaced(Value, TypedValue),
+ Replaced(TypedValue),
}
#[derive(Debug, Clone)]
@@ -32,10 +32,7 @@ impl TypecheckContext {
e: TypedValue,
) -> Result<Self, TypeError> {
let mut vec = self.0.as_ref().clone();
- vec.push((
- x.clone(),
- CtxItem::Replaced(e.to_value(), e.get_type()?.into_owned()),
- ));
+ vec.push((x.clone(), CtxItem::Replaced(e)));
Ok(TypecheckContext(Rc::new(vec)))
}
pub fn lookup(&self, var: &V<Label>) -> Option<TypedValue> {
@@ -45,13 +42,15 @@ impl TypecheckContext {
match var.over_binder(l) {
None => {
let i = i.under_multiple_binders(&shift_map);
- let (th, t) = match i {
+ return Some(match i {
CtxItem::Kept(newvar, t) => {
- (ValueF::Var(newvar).into_value(), t)
+ TypedValue::from_valuef_and_type(
+ ValueF::Var(newvar),
+ t,
+ )
}
- CtxItem::Replaced(th, t) => (th, t),
- };
- return Some(TypedValue::from_value_and_type(th, t));
+ CtxItem::Replaced(v) => v,
+ });
}
Some(newvar) => var = newvar,
};
@@ -114,9 +113,7 @@ impl Shift for CtxItem {
CtxItem::Kept(v, t) => {
CtxItem::Kept(v.shift(delta, var)?, t.shift(delta, var)?)
}
- CtxItem::Replaced(e, t) => {
- CtxItem::Replaced(e.shift(delta, var)?, t.shift(delta, var)?)
- }
+ CtxItem::Replaced(e) => CtxItem::Replaced(e.shift(delta, var)?),
})
}
}
@@ -130,14 +127,9 @@ impl Shift for TypecheckContext {
impl Subst<TypedValue> for CtxItem {
fn subst_shift(&self, var: &AlphaVar, val: &TypedValue) -> Self {
match self {
- CtxItem::Replaced(e, t) => CtxItem::Replaced(
- e.subst_shift(var, val),
- t.subst_shift(var, val),
- ),
+ CtxItem::Replaced(e) => CtxItem::Replaced(e.subst_shift(var, val)),
CtxItem::Kept(v, t) => match v.shift(-1, var) {
- None => {
- CtxItem::Replaced(val.to_value(), t.subst_shift(var, val))
- }
+ None => CtxItem::Replaced(val.clone()),
Some(newvar) => CtxItem::Kept(newvar, t.subst_shift(var, val)),
},
}
diff --git a/dhall/src/core/value.rs b/dhall/src/core/value.rs
index f4cb6b6..c4e3831 100644
--- a/dhall/src/core/value.rs
+++ b/dhall/src/core/value.rs
@@ -2,7 +2,7 @@ use std::borrow::Cow;
use std::cell::{Ref, RefCell, RefMut};
use std::rc::Rc;
-use dhall_syntax::{Const, ExprF};
+use dhall_syntax::Const;
use crate::core::context::TypecheckContext;
use crate::core::valuef::ValueF;
@@ -10,7 +10,7 @@ use crate::core::var::{AlphaVar, Shift, Subst};
use crate::error::{TypeError, TypeMessage};
use crate::phase::normalize::{apply_any, normalize_whnf, OutputSubExpr};
use crate::phase::typecheck::type_of_const;
-use crate::phase::{Normalized, NormalizedSubExpr, Typed};
+use crate::phase::{NormalizedSubExpr, Typed};
#[derive(Debug, Clone, Copy)]
enum Form {
@@ -28,7 +28,7 @@ enum Form {
}
use Form::{Unevaled, NF, WHNF};
-#[derive(Debug, Clone)]
+#[derive(Debug)]
/// 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
@@ -108,7 +108,7 @@ impl ValueInternal {
}
impl Value {
- pub(crate) fn from_valuef(v: ValueF) -> Value {
+ pub(crate) fn from_valuef_untyped(v: ValueF) -> Value {
ValueInternal {
form: Unevaled,
value: v,
@@ -124,18 +124,8 @@ impl Value {
}
.into_value()
}
- pub(crate) fn from_partial_expr(e: ExprF<Value, Normalized>) -> Value {
- Value::from_valuef(ValueF::PartialExpr(e))
- }
- // TODO: avoid using this function
- pub(crate) fn with_type(self, t: TypedValue) -> Value {
- let vint = self.as_internal();
- ValueInternal {
- form: vint.form,
- value: vint.value.clone(),
- ty: Some(t),
- }
- .into_value()
+ pub(crate) fn from_valuef_simple_type(v: ValueF) -> Value {
+ Value::from_valuef_and_type(v, TypedValue::from_const(Const::Type))
}
/// Mutates the contents. If no one else shares this thunk,
@@ -214,7 +204,7 @@ impl Value {
}
pub(crate) fn app_valuef(&self, val: ValueF) -> ValueF {
- self.app_value(val.into_value())
+ self.app_value(val.into_value_untyped())
}
pub(crate) fn app_value(&self, th: Value) -> ValueF {
@@ -227,41 +217,39 @@ impl Value {
}
impl TypedValue {
- pub(crate) fn from_valuef(v: ValueF) -> TypedValue {
- TypedValue::from_value_untyped(Value::from_valuef(v))
- }
-
- pub(crate) fn normalize_nf(&self) -> ValueF {
- self.0.normalize_nf().clone()
- }
-
- pub(crate) fn normalize_to_expr_maybe_alpha(
- &self,
- alpha: bool,
- ) -> OutputSubExpr {
- self.normalize_nf().normalize_to_expr_maybe_alpha(alpha)
+ pub fn from_value(th: Value) -> Self {
+ TypedValue(th)
}
-
- pub(crate) fn from_value_and_type(th: Value, t: TypedValue) -> Self {
- TypedValue(th.with_type(t))
+ pub(crate) fn from_valuef_untyped(v: ValueF) -> TypedValue {
+ TypedValue::from_value(Value::from_valuef_untyped(v))
}
- pub fn from_value_simple_type(th: Value) -> Self {
- TypedValue::from_value_and_type(th, TypedValue::const_type())
+ pub(crate) fn from_valuef_and_type(v: ValueF, t: TypedValue) -> Self {
+ TypedValue(Value::from_valuef_and_type(v, t))
}
- pub(crate) fn from_value_untyped(th: Value) -> Self {
- TypedValue(th)
+ // TODO: do something with the info that the type is Type. Maybe check
+ // is a type is present ?
+ pub(crate) fn from_value_simple_type(th: Value) -> Self {
+ TypedValue::from_value(th)
}
pub(crate) fn from_const(c: Const) -> Self {
match type_of_const(c) {
Ok(t) => TypedValue::from_valuef_and_type(ValueF::Const(c), t),
- Err(_) => TypedValue::from_valuef(ValueF::Const(c)),
+ Err(_) => TypedValue::from_valuef_untyped(ValueF::Const(c)),
}
}
pub fn const_type() -> Self {
TypedValue::from_const(Const::Type)
}
- pub(crate) fn from_valuef_and_type(v: ValueF, t: TypedValue) -> Self {
- TypedValue(Value::from_valuef_and_type(v, t))
+
+ pub(crate) fn normalize_nf(&self) -> ValueF {
+ self.0.normalize_nf().clone()
+ }
+
+ pub(crate) fn normalize_to_expr_maybe_alpha(
+ &self,
+ alpha: bool,
+ ) -> OutputSubExpr {
+ self.normalize_nf().normalize_to_expr_maybe_alpha(alpha)
}
/// WARNING: drop this ref before normalizing the same value or you will run into BorrowMut
diff --git a/dhall/src/core/valuef.rs b/dhall/src/core/valuef.rs
index b948eb1..de55d2f 100644
--- a/dhall/src/core/valuef.rs
+++ b/dhall/src/core/valuef.rs
@@ -48,8 +48,14 @@ pub enum ValueF {
}
impl ValueF {
- pub(crate) fn into_value(self) -> Value {
- Value::from_valuef(self)
+ pub(crate) fn into_value_untyped(self) -> Value {
+ Value::from_valuef_untyped(self)
+ }
+ pub(crate) fn into_value_with_type(self, t: TypedValue) -> Value {
+ Value::from_valuef_and_type(self, t)
+ }
+ pub(crate) fn into_value_simple_type(self) -> Value {
+ Value::from_valuef_simple_type(self)
}
/// Convert the value to a fully normalized syntactic expression
@@ -258,12 +264,12 @@ impl ValueF {
/// Apply to a value
pub(crate) fn app_valuef(self, val: ValueF) -> ValueF {
- self.app_value(val.into_value())
+ self.app_value(val.into_value_untyped())
}
/// Apply to a thunk
pub fn app_value(self, th: Value) -> ValueF {
- Value::from_valuef(self).app_value(th)
+ Value::from_valuef_untyped(self).app_value(th)
}
pub fn from_builtin(b: Builtin) -> ValueF {
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-25 05:31:38 +0000