Rename TyExpr to Tir

5 files changed, 29 insertions, 31 deletions

diff --git a/dhall/src/lib.rs b/dhall/src/lib.rs
index 144cac5..3fbc251 100644
--- a/dhall/src/lib.rs
+++ b/dhall/src/lib.rs
@@ -22,9 +22,7 @@ use crate::error::{EncodeError, Error, TypeError};
 use crate::semantics::parse;
 use crate::semantics::resolve;
 use crate::semantics::resolve::ImportRoot;
-use crate::semantics::{
-    typecheck, typecheck_with, Hir, TyExpr, Value, ValueKind,
-};
+use crate::semantics::{typecheck, typecheck_with, Hir, Tir, Value, ValueKind};
 use crate::syntax::binary;
 use crate::syntax::{Builtin, Expr};
 
@@ -44,7 +42,7 @@ pub struct Resolved(Hir);
 
 /// A typed expression
 #[derive(Debug, Clone)]
-pub struct Typed(TyExpr);
+pub struct Typed(Tir);
 
 /// A normalized expression.
 ///
diff --git a/dhall/src/semantics/resolve/hir.rs b/dhall/src/semantics/resolve/hir.rs
index b5db66f..ae65fff 100644
--- a/dhall/src/semantics/resolve/hir.rs
+++ b/dhall/src/semantics/resolve/hir.rs
@@ -1,5 +1,5 @@
 use crate::error::TypeError;
-use crate::semantics::{type_with, NameEnv, NzEnv, TyEnv, TyExpr, Value};
+use crate::semantics::{type_with, NameEnv, NzEnv, Tir, TyEnv, Value};
 use crate::syntax::{Expr, ExprKind, Span, V};
 use crate::{NormalizedExpr, ToExprOptions};
 
@@ -70,7 +70,7 @@ impl Hir {
     }
 
     /// Typecheck the Hir.
-    pub fn typecheck(&self, env: &TyEnv) -> Result<TyExpr, TypeError> {
+    pub fn typecheck(&self, env: &TyEnv) -> Result<Tir, TypeError> {
         type_with(env, self, None)
     }
 
diff --git a/dhall/src/semantics/tck/mod.rs b/dhall/src/semantics/tck/mod.rs
index 1df2a48..93c8f48 100644
--- a/dhall/src/semantics/tck/mod.rs
+++ b/dhall/src/semantics/tck/mod.rs
@@ -1,6 +1,6 @@
 pub mod env;
-pub mod tyexpr;
+pub mod tir;
 pub mod typecheck;
 pub(crate) use env::*;
-pub(crate) use tyexpr::*;
+pub(crate) use tir::*;
 pub(crate) use typecheck::*;
diff --git a/dhall/src/semantics/tck/tyexpr.rs b/dhall/src/semantics/tck/tir.rs
index f6591ba..800d1b7 100644
--- a/dhall/src/semantics/tck/tyexpr.rs
+++ b/dhall/src/semantics/tck/tir.rs
@@ -15,8 +15,9 @@ pub(crate) struct Type {
 }
 
 /// A hir expression plus its inferred type.
+/// Stands for "Typed intermediate representation"
 #[derive(Debug, Clone)]
-pub(crate) struct TyExpr {
+pub(crate) struct Tir {
     hir: Hir,
     ty: Type,
 }
@@ -105,9 +106,9 @@ impl Type {
     }
 }
 
-impl TyExpr {
+impl Tir {
     pub fn from_hir(hir: &Hir, ty: Type) -> Self {
-        TyExpr {
+        Tir {
             hir: hir.clone(),
             ty,
         }
@@ -134,7 +135,7 @@ impl TyExpr {
         self.as_hir().to_expr_tyenv(env)
     }
 
-    /// Eval the TyExpr. It will actually get evaluated only as needed on demand.
+    /// Eval the Tir. It will actually get evaluated only as needed on demand.
     pub fn eval(&self, env: impl Into<NzEnv>) -> Value {
         self.as_hir().eval(env.into())
     }
@@ -172,12 +173,12 @@ impl TyExpr {
                 .to_universe(),
         ))
     }
-    /// Eval a closed TyExpr (i.e. without free variables). It will actually get evaluated only as
+    /// Eval a closed Tir (i.e. without free variables). It will actually get evaluated only as
     /// needed on demand.
     pub fn eval_closed_expr(&self) -> Value {
         self.eval(NzEnv::new())
     }
-    /// Eval a closed TyExpr fully and recursively;
+    /// Eval a closed Tir fully and recursively;
     pub fn rec_eval_closed_expr(&self) -> Value {
         let val = self.eval_closed_expr();
         val.normalize();
diff --git a/dhall/src/semantics/tck/typecheck.rs b/dhall/src/semantics/tck/typecheck.rs
index 45b3168..7bf15af 100644
--- a/dhall/src/semantics/tck/typecheck.rs
+++ b/dhall/src/semantics/tck/typecheck.rs
@@ -5,8 +5,8 @@ use std::collections::HashMap;
 use crate::error::{ErrorBuilder, TypeError, TypeMessage};
 use crate::semantics::merge_maps;
 use crate::semantics::{
-    type_of_builtin, Binder, BuiltinClosure, Closure, Hir, HirKind, TyEnv,
-    TyExpr, Type, Value, ValueKind,
+    type_of_builtin, Binder, BuiltinClosure, Closure, Hir, HirKind, Tir, TyEnv,
+    Type, Value, ValueKind,
 };
 use crate::syntax::{
     BinOp, Builtin, Const, ExprKind, InterpolatedTextContents, LitKind, Span,
@@ -69,7 +69,7 @@ pub fn mk_span_err<T, S: ToString>(span: Span, msg: S) -> Result<T, TypeError> {
 /// layer.
 fn type_one_layer(
     env: &TyEnv,
-    ekind: ExprKind<TyExpr>,
+    ekind: ExprKind<Tir>,
     span: Span,
 ) -> Result<Type, TypeError> {
     let span_err = |msg: &str| mk_span_err(span.clone(), msg);
@@ -91,8 +91,7 @@ fn type_one_layer(
         ExprKind::Const(Const::Kind) => Type::from_const(Const::Sort),
         ExprKind::Builtin(b) => {
             let t_hir = type_of_builtin(*b);
-            let t_tyexpr = typecheck(&t_hir)?;
-            t_tyexpr.eval_to_type(env)?
+            typecheck(&t_hir)?.eval_to_type(env)?
         }
         ExprKind::Lit(LitKind::Bool(_)) => Type::from_builtin(Builtin::Bool),
         ExprKind::Lit(LitKind::Natural(_)) => {
@@ -712,9 +711,9 @@ pub(crate) fn type_with(
     env: &TyEnv,
     hir: &Hir,
     annot: Option<Type>,
-) -> Result<TyExpr, TypeError> {
-    let tyexpr = match hir.kind() {
-        HirKind::Var(var) => TyExpr::from_hir(hir, env.lookup(var)),
+) -> Result<Tir, TypeError> {
+    let tir = match hir.kind() {
+        HirKind::Var(var) => Tir::from_hir(hir, env.lookup(var)),
         HirKind::Expr(ExprKind::Var(_)) => {
             unreachable!("Hir should contain no unresolved variables")
         }
@@ -753,7 +752,7 @@ pub(crate) fn type_with(
             );
             let ty = Type::new(ty_hir.eval(env), u);
 
-            TyExpr::from_hir(hir, ty)
+            Tir::from_hir(hir, ty)
         }
         HirKind::Expr(ExprKind::Pi(binder, annot, body)) => {
             let annot = type_with(env, annot, None)?;
@@ -765,7 +764,7 @@ pub(crate) fn type_with(
             let ks = annot.ty().as_const().unwrap();
             let kt = body.ty().as_const().unwrap();
             let ty = Type::from_const(function_check(ks, kt));
-            TyExpr::from_hir(hir, ty)
+            Tir::from_hir(hir, ty)
         }
         HirKind::Expr(ExprKind::Let(binder, annot, val, body)) => {
             let val_annot = annot
@@ -777,39 +776,39 @@ pub(crate) fn type_with(
             let body_env = env.insert_value(&binder, val_nf, val.ty().clone());
             let body = type_with(&body_env, body, None)?;
             let ty = body.ty().clone();
-            TyExpr::from_hir(hir, ty)
+            Tir::from_hir(hir, ty)
         }
         HirKind::Expr(ekind) => {
             let ekind = ekind.traverse_ref(|e| type_with(env, e, None))?;
             let ty = type_one_layer(env, ekind, hir.span())?;
-            TyExpr::from_hir(hir, ty)
+            Tir::from_hir(hir, ty)
         }
     };
 
     if let Some(annot) = annot {
-        if *tyexpr.ty() != annot {
+        if *tir.ty() != annot {
             return mk_span_err(
                 hir.span(),
                 &format!(
                     "annot mismatch: {} != {}",
-                    tyexpr.ty().to_expr_tyenv(env),
+                    tir.ty().to_expr_tyenv(env),
                     annot.to_expr_tyenv(env)
                 ),
             );
         }
     }
 
-    Ok(tyexpr)
+    Ok(tir)
 }
 
 /// Typecheck an expression and return the expression annotated with types if type-checking
 /// succeeded, or an error if type-checking failed.
-pub(crate) fn typecheck(hir: &Hir) -> Result<TyExpr, TypeError> {
+pub(crate) fn typecheck(hir: &Hir) -> Result<Tir, TypeError> {
     type_with(&TyEnv::new(), hir, None)
 }
 
 /// Like `typecheck`, but additionally checks that the expression's type matches the provided type.
-pub(crate) fn typecheck_with(hir: &Hir, ty: Hir) -> Result<TyExpr, TypeError> {
+pub(crate) fn typecheck_with(hir: &Hir, ty: Hir) -> Result<Tir, TypeError> {
     let ty = typecheck(&ty)?.eval_to_type(&TyEnv::new())?;
     type_with(&TyEnv::new(), hir, Some(ty))
 }