summaryrefslogtreecommitdiff
path: root/dhall/src/core
diff options
context:
space:
mode:
Diffstat (limited to 'dhall/src/core')
-rw-r--r--dhall/src/core/thunk.rs68
-rw-r--r--dhall/src/core/value.rs24
2 files changed, 47 insertions, 45 deletions
diff --git a/dhall/src/core/thunk.rs b/dhall/src/core/thunk.rs
index 740ecbc..38c54f7 100644
--- a/dhall/src/core/thunk.rs
+++ b/dhall/src/core/thunk.rs
@@ -45,7 +45,7 @@ pub struct Thunk(Rc<RefCell<ThunkInternal>>);
/// A thunk in type position. Can optionally store a Type from the typechecking phase to preserve
/// type information through the normalization phase.
#[derive(Debug, Clone)]
-pub enum TypeThunk {
+pub enum TypedThunk {
// Any value, along with (optionally) its type
Untyped(Thunk),
Typed(Thunk, Box<Type>),
@@ -196,23 +196,23 @@ impl Thunk {
}
}
-impl TypeThunk {
- pub fn from_value(v: Value) -> TypeThunk {
- TypeThunk::from_thunk(Thunk::from_value(v))
+impl TypedThunk {
+ pub fn from_value(v: Value) -> TypedThunk {
+ TypedThunk::from_thunk(Thunk::from_value(v))
}
- pub fn from_thunk(th: Thunk) -> TypeThunk {
- TypeThunk::from_thunk_untyped(th)
+ pub fn from_thunk(th: Thunk) -> TypedThunk {
+ TypedThunk::from_thunk_untyped(th)
}
- pub fn from_type(t: Type) -> TypeThunk {
+ pub fn from_type(t: Type) -> TypedThunk {
t.into_typethunk()
}
pub fn normalize_nf(&self) -> Value {
match self {
- TypeThunk::Const(c) => Value::Const(*c),
- TypeThunk::Untyped(thunk) | TypeThunk::Typed(thunk, _) => {
+ TypedThunk::Const(c) => Value::Const(*c),
+ TypedThunk::Untyped(thunk) | TypedThunk::Typed(thunk, _) => {
thunk.normalize_nf().clone()
}
}
@@ -227,23 +227,23 @@ impl TypeThunk {
}
pub fn from_thunk_and_type(th: Thunk, t: Type) -> Self {
- TypeThunk::Typed(th, Box::new(t))
+ TypedThunk::Typed(th, Box::new(t))
}
pub fn from_thunk_untyped(th: Thunk) -> Self {
- TypeThunk::Untyped(th)
+ TypedThunk::Untyped(th)
}
pub fn from_const(c: Const) -> Self {
- TypeThunk::Const(c)
+ TypedThunk::Const(c)
}
pub fn from_value_untyped(v: Value) -> Self {
- TypeThunk::from_thunk_untyped(Thunk::from_value(v))
+ TypedThunk::from_thunk_untyped(Thunk::from_value(v))
}
// TODO: Avoid cloning if possible
pub fn to_value(&self) -> Value {
match self {
- TypeThunk::Untyped(th) | TypeThunk::Typed(th, _) => th.to_value(),
- TypeThunk::Const(c) => Value::Const(*c),
+ TypedThunk::Untyped(th) | TypedThunk::Typed(th, _) => th.to_value(),
+ TypedThunk::Const(c) => Value::Const(*c),
}
}
pub fn to_expr(&self) -> NormalizedSubExpr {
@@ -254,8 +254,8 @@ impl TypeThunk {
}
pub fn to_thunk(&self) -> Thunk {
match self {
- TypeThunk::Untyped(th) | TypeThunk::Typed(th, _) => th.clone(),
- TypeThunk::Const(c) => Thunk::from_value(Value::Const(*c)),
+ TypedThunk::Untyped(th) | TypedThunk::Typed(th, _) => th.clone(),
+ TypedThunk::Const(c) => Thunk::from_value(Value::Const(*c)),
}
}
pub fn to_type(&self) -> Type {
@@ -274,21 +274,21 @@ impl TypeThunk {
pub fn normalize_mut(&mut self) {
match self {
- TypeThunk::Untyped(th) | TypeThunk::Typed(th, _) => {
+ TypedThunk::Untyped(th) | TypedThunk::Typed(th, _) => {
th.normalize_mut()
}
- TypeThunk::Const(_) => {}
+ TypedThunk::Const(_) => {}
}
}
pub fn get_type(&self) -> Result<Cow<'_, Type>, TypeError> {
match self {
- TypeThunk::Untyped(_) => Err(TypeError::new(
+ TypedThunk::Untyped(_) => Err(TypeError::new(
&TypecheckContext::new(),
TypeMessage::Untyped,
)),
- TypeThunk::Typed(_, t) => Ok(Cow::Borrowed(t)),
- TypeThunk::Const(c) => Ok(Cow::Owned(type_of_const(*c)?)),
+ TypedThunk::Typed(_, t) => Ok(Cow::Borrowed(t)),
+ TypedThunk::Const(c) => Ok(Cow::Owned(type_of_const(*c)?)),
}
}
}
@@ -319,15 +319,17 @@ impl Shift for ThunkInternal {
}
}
-impl Shift for TypeThunk {
+impl Shift for TypedThunk {
fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> {
Some(match self {
- TypeThunk::Untyped(th) => TypeThunk::Untyped(th.shift(delta, var)?),
- TypeThunk::Typed(th, t) => TypeThunk::Typed(
+ TypedThunk::Untyped(th) => {
+ TypedThunk::Untyped(th.shift(delta, var)?)
+ }
+ TypedThunk::Typed(th, t) => TypedThunk::Typed(
th.shift(delta, var)?,
Box::new(t.shift(delta, var)?),
),
- TypeThunk::Const(c) => TypeThunk::Const(*c),
+ TypedThunk::Const(c) => TypedThunk::Const(*c),
})
}
}
@@ -365,17 +367,17 @@ impl Subst<Typed> for ThunkInternal {
}
}
-impl Subst<Typed> for TypeThunk {
+impl Subst<Typed> for TypedThunk {
fn subst_shift(&self, var: &AlphaVar, val: &Typed) -> Self {
match self {
- TypeThunk::Untyped(th) => {
- TypeThunk::Untyped(th.subst_shift(var, val))
+ TypedThunk::Untyped(th) => {
+ TypedThunk::Untyped(th.subst_shift(var, val))
}
- TypeThunk::Typed(th, t) => TypeThunk::Typed(
+ TypedThunk::Typed(th, t) => TypedThunk::Typed(
th.subst_shift(var, val),
Box::new(t.subst_shift(var, val)),
),
- TypeThunk::Const(c) => TypeThunk::Const(*c),
+ TypedThunk::Const(c) => TypedThunk::Const(*c),
}
}
}
@@ -387,9 +389,9 @@ impl std::cmp::PartialEq for Thunk {
}
impl std::cmp::Eq for Thunk {}
-impl std::cmp::PartialEq for TypeThunk {
+impl std::cmp::PartialEq for TypedThunk {
fn eq(&self, other: &Self) -> bool {
self.to_value() == other.to_value()
}
}
-impl std::cmp::Eq for TypeThunk {}
+impl std::cmp::Eq for TypedThunk {}
diff --git a/dhall/src/core/value.rs b/dhall/src/core/value.rs
index 0b68bf6..8486d6e 100644
--- a/dhall/src/core/value.rs
+++ b/dhall/src/core/value.rs
@@ -5,7 +5,7 @@ use dhall_syntax::{
NaiveDouble, Natural, X,
};
-use crate::core::thunk::{Thunk, TypeThunk};
+use crate::core::thunk::{Thunk, TypedThunk};
use crate::core::var::{AlphaLabel, AlphaVar, Shift, Subst};
use crate::phase::normalize::{
apply_builtin, normalize_one_layer, squash_textlit, OutputSubExpr,
@@ -26,15 +26,15 @@ use crate::phase::Typed;
#[derive(Debug, Clone, PartialEq, Eq)]
pub enum Value {
/// Closures
- Lam(AlphaLabel, TypeThunk, Thunk),
- Pi(AlphaLabel, TypeThunk, TypeThunk),
+ Lam(AlphaLabel, TypedThunk, Thunk),
+ Pi(AlphaLabel, TypedThunk, TypedThunk),
// Invariant: the evaluation must not be able to progress further.
AppliedBuiltin(Builtin, Vec<Thunk>),
/// `λ(x: a) -> Some x`
- OptionalSomeClosure(TypeThunk),
+ OptionalSomeClosure(TypedThunk),
/// `λ(x : a) -> λ(xs : List a) -> [ x ] # xs`
/// `λ(xs : List a) -> [ x ] # xs`
- ListConsClosure(TypeThunk, Option<Thunk>),
+ ListConsClosure(TypedThunk, Option<Thunk>),
/// `λ(x : Natural) -> x + 1`
NaturalSuccClosure,
@@ -44,20 +44,20 @@ pub enum Value {
NaturalLit(Natural),
IntegerLit(Integer),
DoubleLit(NaiveDouble),
- EmptyOptionalLit(TypeThunk),
+ EmptyOptionalLit(TypedThunk),
NEOptionalLit(Thunk),
// EmptyListLit(t) means `[] : List t`, not `[] : t`
- EmptyListLit(TypeThunk),
+ EmptyListLit(TypedThunk),
NEListLit(Vec<Thunk>),
RecordLit(HashMap<Label, Thunk>),
- RecordType(HashMap<Label, TypeThunk>),
- UnionType(HashMap<Label, Option<TypeThunk>>),
- UnionConstructor(Label, HashMap<Label, Option<TypeThunk>>),
- UnionLit(Label, Thunk, HashMap<Label, Option<TypeThunk>>),
+ RecordType(HashMap<Label, TypedThunk>),
+ UnionType(HashMap<Label, Option<TypedThunk>>),
+ UnionConstructor(Label, HashMap<Label, Option<TypedThunk>>),
+ UnionLit(Label, Thunk, HashMap<Label, Option<TypedThunk>>),
// Invariant: this must not contain interpolations that are themselves TextLits, and
// contiguous text values must be merged.
TextLit(Vec<InterpolatedTextContents<Thunk>>),
- Equivalence(TypeThunk, TypeThunk),
+ Equivalence(TypedThunk, TypedThunk),
// Invariant: this must not contain a value captured by one of the variants above.
PartialExpr(ExprF<Thunk, X>),
}
generated by cgit v1.2.3 (git 2.25.1) at 2025-01-11 15:35:51 +0000