summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--dhall/src/lib.rs6
-rw-r--r--dhall/src/semantics/resolve/hir.rs4
-rw-r--r--dhall/src/semantics/tck/mod.rs4
-rw-r--r--dhall/src/semantics/tck/tir.rs (renamed from dhall/src/semantics/tck/tyexpr.rs)13
-rw-r--r--dhall/src/semantics/tck/typecheck.rs33
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))
}
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-23 10:04:48 +0000