summaryrefslogtreecommitdiff
path: root/dhall/src/semantics/tck
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--dhall/src/semantics/tck/env.rs8
-rw-r--r--dhall/src/semantics/tck/mod.rs6
-rw-r--r--dhall/src/semantics/tck/tir.rs13
-rw-r--r--dhall/src/semantics/tck/typecheck.rs55
4 files changed, 31 insertions, 51 deletions
diff --git a/dhall/src/semantics/tck/env.rs b/dhall/src/semantics/tck/env.rs
index 6dd5076..1fa66f0 100644
--- a/dhall/src/semantics/tck/env.rs
+++ b/dhall/src/semantics/tck/env.rs
@@ -2,21 +2,21 @@ use crate::semantics::{AlphaVar, NameEnv, Nir, NzEnv, NzVar, Type, ValEnv};
use crate::syntax::Label;
/// Environment for indexing variables.
-#[derive(Debug, Clone, Copy)]
-pub(crate) struct VarEnv {
+#[derive(Debug, Clone, Copy, Default)]
+pub struct VarEnv {
size: usize,
}
/// Environment for typing expressions.
#[derive(Debug, Clone)]
-pub(crate) struct TyEnv {
+pub struct TyEnv {
names: NameEnv,
items: ValEnv<Type>,
}
impl VarEnv {
pub fn new() -> Self {
- VarEnv { size: 0 }
+ VarEnv::default()
}
pub fn from_size(size: usize) -> Self {
VarEnv { size }
diff --git a/dhall/src/semantics/tck/mod.rs b/dhall/src/semantics/tck/mod.rs
index 93c8f48..6dddfc5 100644
--- a/dhall/src/semantics/tck/mod.rs
+++ b/dhall/src/semantics/tck/mod.rs
@@ -1,6 +1,6 @@
pub mod env;
pub mod tir;
pub mod typecheck;
-pub(crate) use env::*;
-pub(crate) use tir::*;
-pub(crate) use typecheck::*;
+pub use env::*;
+pub use tir::*;
+pub use typecheck::*;
diff --git a/dhall/src/semantics/tck/tir.rs b/dhall/src/semantics/tck/tir.rs
index aeb7bf9..89a8027 100644
--- a/dhall/src/semantics/tck/tir.rs
+++ b/dhall/src/semantics/tck/tir.rs
@@ -1,15 +1,14 @@
use crate::error::{ErrorBuilder, TypeError};
use crate::semantics::{mkerr, Hir, Nir, NirKind, NzEnv, TyEnv, VarEnv};
-use crate::syntax::{Builtin, Const, Span};
-use crate::NormalizedExpr;
+use crate::syntax::{Builtin, Const, Expr, Span};
/// The type of a type. 0 is `Type`, 1 is `Kind`, etc...
#[derive(Debug, Copy, Clone, PartialEq, Eq, PartialOrd, Ord, Default)]
-pub(crate) struct Universe(u8);
+pub struct Universe(u8);
/// An expression representing a type
#[derive(Debug, Clone, PartialEq, Eq)]
-pub(crate) struct Type {
+pub struct Type {
val: Nir,
univ: Universe,
}
@@ -17,7 +16,7 @@ pub(crate) struct Type {
/// A hir expression plus its inferred type.
/// Stands for "Typed intermediate representation"
#[derive(Debug, Clone)]
-pub(crate) struct Tir<'hir> {
+pub struct Tir<'hir> {
hir: &'hir Hir,
ty: Type,
}
@@ -101,7 +100,7 @@ impl Type {
pub fn to_hir(&self, venv: VarEnv) -> Hir {
self.val.to_hir(venv)
}
- pub fn to_expr_tyenv(&self, tyenv: &TyEnv) -> NormalizedExpr {
+ pub fn to_expr_tyenv(&self, tyenv: &TyEnv) -> Expr {
self.val.to_hir(tyenv.as_varenv()).to_expr_tyenv(tyenv)
}
}
@@ -124,7 +123,7 @@ impl<'hir> Tir<'hir> {
pub fn as_hir(&self) -> &Hir {
&self.hir
}
- pub fn to_expr_tyenv(&self, env: &TyEnv) -> NormalizedExpr {
+ pub fn to_expr_tyenv(&self, env: &TyEnv) -> Expr {
self.as_hir().to_expr_tyenv(env)
}
diff --git a/dhall/src/semantics/tck/typecheck.rs b/dhall/src/semantics/tck/typecheck.rs
index 173b76d..c3334b5 100644
--- a/dhall/src/semantics/tck/typecheck.rs
+++ b/dhall/src/semantics/tck/typecheck.rs
@@ -5,11 +5,11 @@ 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, Nir,
- NirKind, Tir, TyEnv, Type,
+ type_of_builtin, Binder, Closure, Hir, HirKind, Nir, NirKind, Tir, TyEnv,
+ Type,
};
use crate::syntax::{
- BinOp, Builtin, Const, ExprKind, InterpolatedTextContents, LitKind, Span,
+ BinOp, Builtin, Const, ExprKind, InterpolatedTextContents, NumKind, Span,
};
fn check_rectymerge(
@@ -53,14 +53,11 @@ fn function_check(a: Const, b: Const) -> Const {
}
}
-pub(crate) fn mkerr<T, S: ToString>(msg: S) -> Result<T, TypeError> {
+pub fn mkerr<T, S: ToString>(msg: S) -> Result<T, TypeError> {
Err(TypeError::new(TypeMessage::Custom(msg.to_string())))
}
-pub(crate) fn mk_span_err<T, S: ToString>(
- span: Span,
- msg: S,
-) -> Result<T, TypeError> {
+pub fn mk_span_err<T, S: ToString>(span: Span, msg: S) -> Result<T, TypeError> {
mkerr(
ErrorBuilder::new(msg.to_string())
.span_err(span, msg.to_string())
@@ -96,14 +93,14 @@ fn type_one_layer(
let t_hir = type_of_builtin(*b);
typecheck(&t_hir)?.eval_to_type(env)?
}
- ExprKind::Lit(LitKind::Bool(_)) => Type::from_builtin(Builtin::Bool),
- ExprKind::Lit(LitKind::Natural(_)) => {
+ ExprKind::Num(NumKind::Bool(_)) => Type::from_builtin(Builtin::Bool),
+ ExprKind::Num(NumKind::Natural(_)) => {
Type::from_builtin(Builtin::Natural)
}
- ExprKind::Lit(LitKind::Integer(_)) => {
+ ExprKind::Num(NumKind::Integer(_)) => {
Type::from_builtin(Builtin::Integer)
}
- ExprKind::Lit(LitKind::Double(_)) => {
+ ExprKind::Num(NumKind::Double(_)) => {
Type::from_builtin(Builtin::Double)
}
ExprKind::TextLit(interpolated) => {
@@ -121,11 +118,7 @@ fn type_one_layer(
ExprKind::EmptyListLit(t) => {
let t = t.eval_to_type(env)?;
match t.kind() {
- NirKind::AppliedBuiltin(BuiltinClosure {
- b: Builtin::List,
- args,
- ..
- }) if args.len() == 1 => {}
+ NirKind::ListType(..) => {}
_ => return span_err("InvalidListType"),
};
t
@@ -376,10 +369,7 @@ fn type_one_layer(
}
ExprKind::BinOp(BinOp::ListAppend, l, r) => {
match l.ty().kind() {
- NirKind::AppliedBuiltin(BuiltinClosure {
- b: Builtin::List,
- ..
- }) => {}
+ NirKind::ListType(..) => {}
_ => return span_err("BinOpTypeMismatch"),
}
@@ -435,12 +425,7 @@ fn type_one_layer(
let union_type = union.ty();
let variants = match union_type.kind() {
NirKind::UnionType(kts) => Cow::Borrowed(kts),
- NirKind::AppliedBuiltin(BuiltinClosure {
- b: Builtin::Optional,
- args,
- ..
- }) if args.len() == 1 => {
- let ty = &args[0];
+ NirKind::OptionalType(ty) => {
let mut kts = HashMap::new();
kts.insert("None".into(), None);
kts.insert("Some".into(), Some(ty.clone()));
@@ -595,11 +580,7 @@ fn type_one_layer(
let err_msg = "The type of `toMap x` must be of the form \
`List { mapKey : Text, mapValue : T }`";
let arg = match annot_val.kind() {
- NirKind::AppliedBuiltin(BuiltinClosure {
- b: Builtin::List,
- args,
- ..
- }) if args.len() == 1 => &args[0],
+ NirKind::ListType(t) => t,
_ => return span_err(err_msg),
};
let kts = match arg.kind() {
@@ -704,7 +685,7 @@ fn type_one_layer(
/// `type_with` typechecks an expression in the provided environment. Optionally pass an annotation
/// to compare with.
-pub(crate) fn type_with<'hir>(
+pub fn type_with<'hir>(
env: &TyEnv,
hir: &'hir Hir,
annot: Option<Type>,
@@ -801,15 +782,15 @@ pub(crate) fn type_with<'hir>(
/// 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: &'hir Hir) -> Result<Tir<'hir>, TypeError> {
+pub fn typecheck<'hir>(hir: &'hir Hir) -> Result<Tir<'hir>, 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>(
+pub fn typecheck_with<'hir>(
hir: &'hir Hir,
- ty: Hir,
+ ty: &Hir,
) -> Result<Tir<'hir>, TypeError> {
- let ty = typecheck(&ty)?.eval_to_type(&TyEnv::new())?;
+ 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-26 22:09:02 +0000