s/TypeThunk/TypedThunk/g

5 files changed, 96 insertions, 86 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>),
 }
diff --git a/dhall/src/phase/mod.rs b/dhall/src/phase/mod.rs
index 0b05227..27a6901 100644
--- a/dhall/src/phase/mod.rs
+++ b/dhall/src/phase/mod.rs
@@ -4,7 +4,7 @@ use std::path::Path;
 
 use dhall_syntax::{Const, Import, Span, SubExpr, X};
 
-use crate::core::thunk::{Thunk, TypeThunk};
+use crate::core::thunk::{Thunk, TypedThunk};
 use crate::core::value::Value;
 use crate::core::var::{AlphaVar, Shift, Subst};
 use crate::error::{EncodeError, Error, ImportError, TypeError};
@@ -31,7 +31,7 @@ pub struct Resolved(ResolvedSubExpr);
 
 /// A typed expression
 #[derive(Debug, Clone)]
-pub struct Typed(TypeThunk);
+pub struct Typed(TypedThunk);
 
 /// A normalized expression.
 ///
@@ -100,18 +100,18 @@ impl Typed {
     }
 
     pub fn from_thunk_and_type(th: Thunk, t: Type) -> Self {
-        Typed(TypeThunk::from_thunk_and_type(th, t))
+        Typed(TypedThunk::from_thunk_and_type(th, t))
     }
     pub fn from_thunk_untyped(th: Thunk) -> Self {
-        Typed(TypeThunk::from_thunk_untyped(th))
+        Typed(TypedThunk::from_thunk_untyped(th))
     }
     pub fn from_const(c: Const) -> Self {
-        Typed(TypeThunk::from_const(c))
+        Typed(TypedThunk::from_const(c))
     }
     pub fn from_value_untyped(v: Value) -> Self {
-        Typed(TypeThunk::from_value_untyped(v))
+        Typed(TypedThunk::from_value_untyped(v))
     }
-    pub fn from_typethunk(th: TypeThunk) -> Self {
+    pub fn from_typethunk(th: TypedThunk) -> Self {
         Typed(th)
     }
 
@@ -135,7 +135,7 @@ impl Typed {
     pub fn into_type(self) -> Type {
         self
     }
-    pub fn into_typethunk(self) -> TypeThunk {
+    pub fn into_typethunk(self) -> TypedThunk {
         self.0
     }
     pub fn to_normalized(&self) -> Normalized {
diff --git a/dhall/src/phase/normalize.rs b/dhall/src/phase/normalize.rs
index 405677a..644f98c 100644
--- a/dhall/src/phase/normalize.rs
+++ b/dhall/src/phase/normalize.rs
@@ -6,7 +6,7 @@ use dhall_syntax::{
 };
 
 use crate::core::context::NormalizationContext;
-use crate::core::thunk::{Thunk, TypeThunk};
+use crate::core::thunk::{Thunk, TypedThunk};
 use crate::core::value::Value;
 use crate::core::var::Subst;
 use crate::phase::{NormalizedSubExpr, ResolvedSubExpr, Typed};
@@ -22,7 +22,7 @@ pub fn apply_builtin(b: Builtin, args: Vec<Thunk>) -> Value {
     // Return Ok((unconsumed args, returned value)), or Err(()) if value could not be produced.
     let ret = match (b, args.as_slice()) {
         (OptionalNone, [t, r..]) => {
-            Ok((r, EmptyOptionalLit(TypeThunk::from_thunk(t.clone()))))
+            Ok((r, EmptyOptionalLit(TypedThunk::from_thunk(t.clone()))))
         }
         (NaturalIsZero, [n, r..]) => match &*n.as_value() {
             NaturalLit(n) => Ok((r, BoolLit(*n == 0))),
@@ -144,10 +144,10 @@ pub fn apply_builtin(b: Builtin, args: Vec<Thunk>) -> Value {
                 let mut kts = HashMap::new();
                 kts.insert(
                     "index".into(),
-                    TypeThunk::from_value(Value::from_builtin(Natural)),
+                    TypedThunk::from_value(Value::from_builtin(Natural)),
                 );
                 kts.insert("value".into(), t.clone());
-                Ok((r, EmptyListLit(TypeThunk::from_value(RecordType(kts)))))
+                Ok((r, EmptyListLit(TypedThunk::from_value(RecordType(kts)))))
             }
             NEListLit(xs) => {
                 let xs = xs
@@ -179,10 +179,10 @@ pub fn apply_builtin(b: Builtin, args: Vec<Thunk>) -> Value {
                 r,
                 f.app_val(Value::from_builtin(List).app_thunk(t.clone()))
                     .app_val(ListConsClosure(
-                        TypeThunk::from_thunk(t.clone()),
+                        TypedThunk::from_thunk(t.clone()),
                         None,
                     ))
-                    .app_val(EmptyListLit(TypeThunk::from_thunk(t.clone()))),
+                    .app_val(EmptyListLit(TypedThunk::from_thunk(t.clone()))),
             )),
         },
         (ListFold, [_, l, _, cons, nil, r..]) => match &*l.as_value() {
@@ -213,10 +213,10 @@ pub fn apply_builtin(b: Builtin, args: Vec<Thunk>) -> Value {
             _ => Ok((
                 r,
                 f.app_val(Value::from_builtin(Optional).app_thunk(t.clone()))
-                    .app_val(OptionalSomeClosure(TypeThunk::from_thunk(
+                    .app_val(OptionalSomeClosure(TypedThunk::from_thunk(
                         t.clone(),
                     )))
-                    .app_val(EmptyOptionalLit(TypeThunk::from_thunk(
+                    .app_val(EmptyOptionalLit(TypedThunk::from_thunk(
                         t.clone(),
                     ))),
             )),
@@ -618,7 +618,7 @@ fn apply_binop<'a>(o: BinOp, x: &'a Thunk, y: &'a Thunk) -> Option<Ret<'a>> {
         }
         (RecursiveRecordTypeMerge, RecordType(kvs1), RecordType(kvs2)) => {
             let kvs = merge_maps(kvs1, kvs2, |v1, v2| {
-                TypeThunk::from_thunk(Thunk::from_partial_expr(ExprF::BinOp(
+                TypedThunk::from_thunk(Thunk::from_partial_expr(ExprF::BinOp(
                     RecursiveRecordTypeMerge,
                     v1.to_thunk(),
                     v2.to_thunk(),
@@ -628,8 +628,8 @@ fn apply_binop<'a>(o: BinOp, x: &'a Thunk, y: &'a Thunk) -> Option<Ret<'a>> {
         }
 
         (Equivalence, _, _) => Ret::Value(Value::Equivalence(
-            TypeThunk::from_thunk(x.clone()),
-            TypeThunk::from_thunk(y.clone()),
+            TypedThunk::from_thunk(x.clone()),
+            TypedThunk::from_thunk(y.clone()),
         )),
 
         _ => return None,
@@ -649,12 +649,12 @@ pub fn normalize_one_layer(expr: ExprF<Thunk, X>) -> Value {
         ExprF::Annot(x, _) => Ret::Thunk(x),
         ExprF::Assert(_) => Ret::Expr(expr),
         ExprF::Lam(x, t, e) => {
-            Ret::Value(Lam(x.into(), TypeThunk::from_thunk(t), e))
+            Ret::Value(Lam(x.into(), TypedThunk::from_thunk(t), e))
         }
         ExprF::Pi(x, t, e) => Ret::Value(Pi(
             x.into(),
-            TypeThunk::from_thunk(t),
-            TypeThunk::from_thunk(e),
+            TypedThunk::from_thunk(t),
+            TypedThunk::from_thunk(e),
         )),
         ExprF::Let(x, _, v, b) => {
             let v = Typed::from_thunk_untyped(v);
@@ -673,7 +673,7 @@ pub fn normalize_one_layer(expr: ExprF<Thunk, X>) -> Value {
             let t_borrow = t.as_value();
             match &*t_borrow {
                 AppliedBuiltin(Builtin::List, args) if args.len() == 1 => {
-                    Ret::Value(EmptyListLit(TypeThunk::from_thunk(
+                    Ret::Value(EmptyListLit(TypedThunk::from_thunk(
                         args[0].clone(),
                     )))
                 }
@@ -691,12 +691,12 @@ pub fn normalize_one_layer(expr: ExprF<Thunk, X>) -> Value {
         }
         ExprF::RecordType(kts) => Ret::Value(RecordType(
             kts.into_iter()
-                .map(|(k, t)| (k, TypeThunk::from_thunk(t)))
+                .map(|(k, t)| (k, TypedThunk::from_thunk(t)))
                 .collect(),
         )),
         ExprF::UnionType(kts) => Ret::Value(UnionType(
             kts.into_iter()
-                .map(|(k, t)| (k, t.map(|t| TypeThunk::from_thunk(t))))
+                .map(|(k, t)| (k, t.map(|t| TypedThunk::from_thunk(t))))
                 .collect(),
         )),
         ExprF::TextLit(elts) => {
diff --git a/dhall/src/phase/typecheck.rs b/dhall/src/phase/typecheck.rs
index 299997a..a19e1ca 100644
--- a/dhall/src/phase/typecheck.rs
+++ b/dhall/src/phase/typecheck.rs
@@ -6,7 +6,7 @@ use dhall_syntax::{
 };
 
 use crate::core::context::{NormalizationContext, TypecheckContext};
-use crate::core::thunk::{Thunk, TypeThunk};
+use crate::core::thunk::{Thunk, TypedThunk};
 use crate::core::value::Value;
 use crate::core::var::{Shift, Subst};
 use crate::error::{TypeError, TypeMessage};
@@ -44,8 +44,12 @@ fn tck_pi_type(
     let k = function_check(ka, kb);
 
     Ok(Typed::from_thunk_and_type(
-        Value::Pi(x.into(), TypeThunk::from_type(tx), TypeThunk::from_type(te))
-            .into_thunk(),
+        Value::Pi(
+            x.into(),
+            TypedThunk::from_type(tx),
+            TypedThunk::from_type(te),
+        )
+        .into_thunk(),
         Type::from_const(k),
     ))
 }
@@ -77,7 +81,7 @@ fn tck_record_type(
                 return Err(TypeError::new(ctx, RecordTypeDuplicateField))
             }
             Entry::Vacant(_) => {
-                entry.or_insert_with(|| TypeThunk::from_type(t.clone()))
+                entry.or_insert_with(|| TypedThunk::from_type(t.clone()))
             }
         };
     }
@@ -119,7 +123,7 @@ fn tck_union_type(
                 return Err(TypeError::new(ctx, UnionTypeDuplicateField))
             }
             Entry::Vacant(_) => entry.or_insert_with(|| {
-                t.as_ref().map(|t| TypeThunk::from_type(t.clone()))
+                t.as_ref().map(|t| TypedThunk::from_type(t.clone()))
             }),
         };
     }
@@ -334,7 +338,7 @@ fn type_with(
             let b = type_with(&ctx2, b.clone())?;
             let v = Value::Lam(
                 x.clone().into(),
-                TypeThunk::from_type(tx.clone()),
+                TypedThunk::from_type(tx.clone()),
                 b.to_thunk(),
             );
             let tb = b.get_type()?.into_owned();
@@ -658,8 +662,8 @@ fn type_last_layer(
             // records of records when merging.
             fn combine_record_types(
                 ctx: &TypecheckContext,
-                kts_l: HashMap<Label, TypeThunk>,
-                kts_r: HashMap<Label, TypeThunk>,
+                kts_l: HashMap<Label, TypedThunk>,
+                kts_r: HashMap<Label, TypedThunk>,
             ) -> Result<Typed, TypeError> {
                 use crate::phase::normalize::outer_join;
 
@@ -667,8 +671,8 @@ fn type_last_layer(
                 // are records themselves, then we hit the recursive case.
                 // Otherwise we have a field collision.
                 let combine = |k: &Label,
-                               inner_l: &TypeThunk,
-                               inner_r: &TypeThunk|
+                               inner_l: &TypedThunk,
+                               inner_r: &TypedThunk|
                  -> Result<Typed, TypeError> {
                     match (inner_l.to_value(), inner_r.to_value()) {
                         (
@@ -686,7 +690,9 @@ fn type_last_layer(
                 let kts: HashMap<Label, Result<Typed, TypeError>> = outer_join(
                     |l| Ok(l.to_type()),
                     |r| Ok(r.to_type()),
-                    |k: &Label, l: &TypeThunk, r: &TypeThunk| combine(k, l, r),
+                    |k: &Label, l: &TypedThunk, r: &TypedThunk| {
+                        combine(k, l, r)
+                    },
                     &kts_l,
                     &kts_r,
                 );
@@ -729,8 +735,8 @@ fn type_last_layer(
             // records of records when merging.
             fn combine_record_types(
                 ctx: &TypecheckContext,
-                kts_l: HashMap<Label, TypeThunk>,
-                kts_r: HashMap<Label, TypeThunk>,
+                kts_l: HashMap<Label, TypedThunk>,
+                kts_r: HashMap<Label, TypedThunk>,
             ) -> Result<Typed, TypeError> {
                 use crate::phase::normalize::intersection_with_key;
 
@@ -738,8 +744,8 @@ fn type_last_layer(
                 // are records themselves, then we hit the recursive case.
                 // Otherwise we have a field collision.
                 let combine = |k: &Label,
-                               kts_l_inner: &TypeThunk,
-                               kts_r_inner: &TypeThunk|
+                               kts_l_inner: &TypedThunk,
+                               kts_r_inner: &TypedThunk|
                  -> Result<Typed, TypeError> {
                     match (kts_l_inner.to_value(), kts_r_inner.to_value()) {
                         (
@@ -755,7 +761,9 @@ fn type_last_layer(
                 };
 
                 let kts = intersection_with_key(
-                    |k: &Label, l: &TypeThunk, r: &TypeThunk| combine(k, l, r),
+                    |k: &Label, l: &TypedThunk, r: &TypedThunk| {
+                        combine(k, l, r)
+                    },
                     &kts_l,
                     &kts_r,
                 );