summaryrefslogtreecommitdiff
path: root/dhall/src/core
diff options
context:
space:
mode:
authorNadrieril2019-08-19 21:52:26 +0200
committerNadrieril2019-08-19 21:52:42 +0200
commit26a1fd0f0861038a76a0f9b09eaef16d808d4139 (patch)
treee89770d190a73ce5f1bae7798b77c02b598faed2 /dhall/src/core
parent29016b78736dca857e4e7f7c4dc68ed5e30c28bb (diff)
Use TypedValue instead of Typed in normalize and typecheck
Now Typed is only used in dhall::phase, similarly to Parsed/Resolved/Normalized
Diffstat (limited to 'dhall/src/core')
-rw-r--r--dhall/src/core/context.rs29
-rw-r--r--dhall/src/core/value.rs48
-rw-r--r--dhall/src/core/valuef.rs6
3 files changed, 39 insertions, 44 deletions
diff --git a/dhall/src/core/context.rs b/dhall/src/core/context.rs
index e1a23a9..851e4c4 100644
--- a/dhall/src/core/context.rs
+++ b/dhall/src/core/context.rs
@@ -3,16 +3,15 @@ use std::rc::Rc;
use dhall_syntax::{Label, V};
-use crate::core::value::Value;
+use crate::core::value::{TypedValue, Value};
use crate::core::valuef::ValueF;
use crate::core::var::{AlphaVar, Shift, Subst};
use crate::error::TypeError;
-use crate::phase::{Type, Typed};
#[derive(Debug, Clone)]
enum CtxItem {
- Kept(AlphaVar, Type),
- Replaced(Value, Type),
+ Kept(AlphaVar, TypedValue),
+ Replaced(Value, TypedValue),
}
#[derive(Debug, Clone)]
@@ -22,12 +21,16 @@ impl TypecheckContext {
pub fn new() -> Self {
TypecheckContext(Rc::new(Vec::new()))
}
- pub fn insert_type(&self, x: &Label, t: Type) -> Self {
+ pub fn insert_type(&self, x: &Label, t: TypedValue) -> 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: Typed) -> Result<Self, TypeError> {
+ pub fn insert_value(
+ &self,
+ x: &Label,
+ e: TypedValue,
+ ) -> Result<Self, TypeError> {
let mut vec = self.0.as_ref().clone();
vec.push((
x.clone(),
@@ -35,7 +38,7 @@ impl TypecheckContext {
));
Ok(TypecheckContext(Rc::new(vec)))
}
- pub fn lookup(&self, var: &V<Label>) -> Option<Typed> {
+ pub fn lookup(&self, var: &V<Label>) -> Option<TypedValue> {
let mut var = var.clone();
let mut shift_map: HashMap<Label, _> = HashMap::new();
for (l, i) in self.0.iter().rev() {
@@ -48,7 +51,7 @@ impl TypecheckContext {
}
CtxItem::Replaced(th, t) => (th, t),
};
- return Some(Typed::from_value_and_type(th, t));
+ return Some(TypedValue::from_value_and_type(th, t));
}
Some(newvar) => var = newvar,
};
@@ -99,7 +102,7 @@ impl TypecheckContext {
)))
}
}
- fn subst_shift(&self, var: &AlphaVar, val: &Typed) -> Self {
+ fn subst_shift(&self, var: &AlphaVar, val: &TypedValue) -> Self {
self.do_with_var(var, |var, i| Ok::<_, !>(i.subst_shift(&var, val)))
.unwrap()
}
@@ -124,8 +127,8 @@ impl Shift for TypecheckContext {
}
}
-impl Subst<Typed> for CtxItem {
- fn subst_shift(&self, var: &AlphaVar, val: &Typed) -> Self {
+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),
@@ -141,8 +144,8 @@ impl Subst<Typed> for CtxItem {
}
}
-impl Subst<Typed> for TypecheckContext {
- fn subst_shift(&self, var: &AlphaVar, val: &Typed) -> Self {
+impl Subst<TypedValue> for TypecheckContext {
+ fn subst_shift(&self, var: &AlphaVar, val: &TypedValue) -> Self {
self.subst_shift(var, val)
}
}
diff --git a/dhall/src/core/value.rs b/dhall/src/core/value.rs
index 213a2bd..f4cb6b6 100644
--- a/dhall/src/core/value.rs
+++ b/dhall/src/core/value.rs
@@ -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, Type, Typed};
+use crate::phase::{Normalized, NormalizedSubExpr, Typed};
#[derive(Debug, Clone, Copy)]
enum Form {
@@ -35,12 +35,12 @@ use Form::{Unevaled, NF, WHNF};
struct ValueInternal {
form: Form,
value: ValueF,
- ty: Option<Type>,
+ ty: Option<TypedValue>,
}
/// 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 through
+/// Can optionally store a type from typechecking to preserve type information through
/// normalization.
#[derive(Clone)]
pub struct Value(Rc<RefCell<ValueInternal>>);
@@ -96,7 +96,7 @@ impl ValueInternal {
}
}
- fn get_type(&self) -> Result<&Type, TypeError> {
+ fn get_type(&self) -> Result<&TypedValue, TypeError> {
match &self.ty {
Some(t) => Ok(t),
None => Err(TypeError::new(
@@ -116,7 +116,7 @@ impl Value {
}
.into_value()
}
- pub(crate) fn from_valuef_and_type(v: ValueF, t: Type) -> Value {
+ pub(crate) fn from_valuef_and_type(v: ValueF, t: TypedValue) -> Value {
ValueInternal {
form: Unevaled,
value: v,
@@ -128,7 +128,7 @@ impl Value {
Value::from_valuef(ValueF::PartialExpr(e))
}
// TODO: avoid using this function
- pub(crate) fn with_type(self, t: Type) -> Value {
+ pub(crate) fn with_type(self, t: TypedValue) -> Value {
let vint = self.as_internal();
ValueInternal {
form: vint.form,
@@ -221,7 +221,7 @@ impl Value {
apply_any(self.clone(), th)
}
- pub(crate) fn get_type(&self) -> Result<Cow<'_, Type>, TypeError> {
+ pub(crate) fn get_type(&self) -> Result<Cow<'_, TypedValue>, TypeError> {
Ok(Cow::Owned(self.as_internal().get_type()?.clone()))
}
}
@@ -231,18 +231,10 @@ impl TypedValue {
TypedValue::from_value_untyped(Value::from_valuef(v))
}
- pub(crate) fn from_type(t: Type) -> TypedValue {
- t.into_typedvalue()
- }
-
pub(crate) fn normalize_nf(&self) -> ValueF {
self.0.normalize_nf().clone()
}
- pub(crate) fn to_typed(&self) -> Typed {
- self.clone().into_typed()
- }
-
pub(crate) fn normalize_to_expr_maybe_alpha(
&self,
alpha: bool,
@@ -250,11 +242,11 @@ impl TypedValue {
self.normalize_nf().normalize_to_expr_maybe_alpha(alpha)
}
- pub(crate) fn from_value_and_type(th: Value, t: Type) -> Self {
+ pub(crate) fn from_value_and_type(th: Value, t: TypedValue) -> Self {
TypedValue(th.with_type(t))
}
pub fn from_value_simple_type(th: Value) -> Self {
- TypedValue::from_value_and_type(th, Type::const_type())
+ TypedValue::from_value_and_type(th, TypedValue::const_type())
}
pub(crate) fn from_value_untyped(th: Value) -> Self {
TypedValue(th)
@@ -265,7 +257,10 @@ impl TypedValue {
Err(_) => TypedValue::from_valuef(ValueF::Const(c)),
}
}
- pub(crate) fn from_valuef_and_type(v: ValueF, t: Type) -> Self {
+ 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))
}
@@ -286,9 +281,6 @@ impl TypedValue {
pub(crate) fn to_value(&self) -> Value {
self.0.clone()
}
- pub(crate) fn to_type(&self) -> Type {
- self.clone().into_typed().into_type()
- }
pub(crate) fn into_typed(self) -> Typed {
Typed::from_typedvalue(self)
}
@@ -303,7 +295,7 @@ impl TypedValue {
self.0.normalize_mut()
}
- pub(crate) fn get_type(&self) -> Result<Cow<'_, Type>, TypeError> {
+ pub(crate) fn get_type(&self) -> Result<Cow<'_, TypedValue>, TypeError> {
self.0.get_type()
}
}
@@ -330,14 +322,14 @@ impl Shift for TypedValue {
}
}
-impl Subst<Typed> for Value {
- fn subst_shift(&self, var: &AlphaVar, val: &Typed) -> Self {
+impl Subst<TypedValue> for Value {
+ fn subst_shift(&self, var: &AlphaVar, val: &TypedValue) -> Self {
Value(self.0.subst_shift(var, val))
}
}
-impl Subst<Typed> for ValueInternal {
- fn subst_shift(&self, var: &AlphaVar, val: &Typed) -> Self {
+impl Subst<TypedValue> for ValueInternal {
+ fn subst_shift(&self, var: &AlphaVar, val: &TypedValue) -> Self {
ValueInternal {
// The resulting value may not stay in wnhf after substitution
form: Unevaled,
@@ -347,8 +339,8 @@ impl Subst<Typed> for ValueInternal {
}
}
-impl Subst<Typed> for TypedValue {
- fn subst_shift(&self, var: &AlphaVar, val: &Typed) -> Self {
+impl Subst<TypedValue> for TypedValue {
+ fn subst_shift(&self, var: &AlphaVar, val: &TypedValue) -> Self {
TypedValue(self.0.subst_shift(var, val))
}
}
diff --git a/dhall/src/core/valuef.rs b/dhall/src/core/valuef.rs
index 0ba1d59..b948eb1 100644
--- a/dhall/src/core/valuef.rs
+++ b/dhall/src/core/valuef.rs
@@ -8,7 +8,7 @@ use dhall_syntax::{
use crate::core::value::{TypedValue, Value};
use crate::core::var::{AlphaLabel, AlphaVar, Shift, Subst};
use crate::phase::normalize::OutputSubExpr;
-use crate::phase::{Normalized, Typed};
+use crate::phase::Normalized;
/// A semantic value. Subexpressions are Values, which are partially evaluated expressions that are
/// normalized on-demand.
@@ -327,8 +327,8 @@ impl Shift for ValueF {
}
}
-impl Subst<Typed> for ValueF {
- fn subst_shift(&self, var: &AlphaVar, val: &Typed) -> Self {
+impl Subst<TypedValue> for ValueF {
+ fn subst_shift(&self, var: &AlphaVar, val: &TypedValue) -> Self {
match self {
ValueF::AppliedBuiltin(b, args) => {
ValueF::AppliedBuiltin(*b, args.subst_shift(var, val))