summaryrefslogtreecommitdiff
path: root/dhall/src/semantics/tck
diff options
context:
space:
mode:
Diffstat (limited to 'dhall/src/semantics/tck')
-rw-r--r--dhall/src/semantics/tck/env.rs16
-rw-r--r--dhall/src/semantics/tck/tir.rs60
-rw-r--r--dhall/src/semantics/tck/typecheck.rs60
3 files changed, 73 insertions, 63 deletions
diff --git a/dhall/src/semantics/tck/env.rs b/dhall/src/semantics/tck/env.rs
index fc0ce9f..fdcc62d 100644
--- a/dhall/src/semantics/tck/env.rs
+++ b/dhall/src/semantics/tck/env.rs
@@ -13,7 +13,7 @@ pub struct VarEnv {
pub struct TyEnv<'cx> {
cx: Ctxt<'cx>,
names: NameEnv,
- items: ValEnv<Type>,
+ items: ValEnv<'cx, Type<'cx>>,
}
impl VarEnv {
@@ -45,7 +45,7 @@ impl<'cx> TyEnv<'cx> {
TyEnv {
cx,
names: NameEnv::new(),
- items: ValEnv::new(),
+ items: ValEnv::new(cx),
}
}
pub fn cx(&self) -> Ctxt<'cx> {
@@ -54,34 +54,34 @@ impl<'cx> TyEnv<'cx> {
pub fn as_varenv(&self) -> VarEnv {
self.names.as_varenv()
}
- pub fn to_nzenv(&self) -> NzEnv {
+ pub fn to_nzenv(&self) -> NzEnv<'cx> {
self.items.discard_types()
}
pub fn as_nameenv(&self) -> &NameEnv {
&self.names
}
- pub fn insert_type(&self, x: &Label, ty: Type) -> Self {
+ pub fn insert_type(&self, x: &Label, ty: Type<'cx>) -> Self {
TyEnv {
cx: self.cx,
names: self.names.insert(x),
items: self.items.insert_type(ty),
}
}
- pub fn insert_value(&self, x: &Label, e: Nir, ty: Type) -> Self {
+ pub fn insert_value(&self, x: &Label, e: Nir<'cx>, ty: Type<'cx>) -> Self {
TyEnv {
cx: self.cx,
names: self.names.insert(x),
items: self.items.insert_value(e, ty),
}
}
- pub fn lookup(&self, var: AlphaVar) -> Type {
+ pub fn lookup(&self, var: AlphaVar) -> Type<'cx> {
self.items.lookup_ty(var)
}
}
-impl<'a, 'cx> From<&'a TyEnv<'cx>> for NzEnv {
- fn from(x: &'a TyEnv) -> Self {
+impl<'a, 'cx> From<&'a TyEnv<'cx>> for NzEnv<'cx> {
+ fn from(x: &'a TyEnv<'cx>) -> Self {
x.to_nzenv()
}
}
diff --git a/dhall/src/semantics/tck/tir.rs b/dhall/src/semantics/tck/tir.rs
index f34802c..7b04f57 100644
--- a/dhall/src/semantics/tck/tir.rs
+++ b/dhall/src/semantics/tck/tir.rs
@@ -2,6 +2,7 @@ use crate::builtins::Builtin;
use crate::error::{ErrorBuilder, TypeError};
use crate::semantics::{mkerr, Hir, Nir, NirKind, NzEnv, TyEnv, VarEnv};
use crate::syntax::{Const, Expr, Span};
+use crate::Ctxt;
/// The type of a type. 0 is `Type`, 1 is `Kind`, etc...
#[derive(Debug, Copy, Clone, PartialEq, Eq, PartialOrd, Ord, Default)]
@@ -9,17 +10,17 @@ pub struct Universe(u8);
/// An expression representing a type
#[derive(Debug, Clone, PartialEq, Eq)]
-pub struct Type {
- val: Nir,
+pub struct Type<'cx> {
+ val: Nir<'cx>,
univ: Universe,
}
/// A hir expression plus its inferred type.
/// Stands for "Typed intermediate representation"
#[derive(Debug, Clone)]
-pub struct Tir<'hir> {
- hir: &'hir Hir,
- ty: Type,
+pub struct Tir<'cx, 'hir> {
+ hir: &'hir Hir<'cx>,
+ ty: Type<'cx>,
}
impl Universe {
@@ -43,16 +44,16 @@ impl Universe {
}
}
-impl Type {
- pub fn new(val: Nir, univ: Universe) -> Self {
+impl<'cx> Type<'cx> {
+ pub fn new(val: Nir<'cx>, univ: Universe) -> Self {
Type { val, univ }
}
/// Creates a new Type and infers its universe by re-typechecking its value.
/// TODO: ideally avoid this function altogether. Would need to store types in RecordType and
/// PiClosure.
pub fn new_infer_universe(
- env: &TyEnv,
- val: Nir,
+ env: &TyEnv<'cx>,
+ val: Nir<'cx>,
) -> Result<Self, TypeError> {
let c = val.to_hir(env.as_varenv()).typecheck(env)?.ty().as_const();
let u = match c {
@@ -67,14 +68,14 @@ impl Type {
pub fn from_const(c: Const) -> Self {
Self::new(Nir::from_const(c), c.to_universe().next())
}
- pub fn from_builtin(b: Builtin) -> Self {
+ pub fn from_builtin(cx: Ctxt<'cx>, b: Builtin) -> Self {
use Builtin::*;
match b {
Bool | Natural | Integer | Double | Text => {}
_ => unreachable!("this builtin is not a type: {}", b),
}
- Self::new(Nir::from_builtin(b), Universe::from_const(Const::Type))
+ Self::new(Nir::from_builtin(cx, b), Universe::from_const(Const::Type))
}
/// Get the type of this type
@@ -82,60 +83,60 @@ impl Type {
self.univ
}
- pub fn to_nir(&self) -> Nir {
+ pub fn to_nir(&self) -> Nir<'cx> {
self.val.clone()
}
- pub fn as_nir(&self) -> &Nir {
+ pub fn as_nir(&self) -> &Nir<'cx> {
&self.val
}
- pub fn into_nir(self) -> Nir {
+ pub fn into_nir(self) -> Nir<'cx> {
self.val
}
pub fn as_const(&self) -> Option<Const> {
self.val.as_const()
}
- pub fn kind(&self) -> &NirKind {
+ pub fn kind(&self) -> &NirKind<'cx> {
self.val.kind()
}
- pub fn to_hir(&self, venv: VarEnv) -> Hir {
+ pub fn to_hir(&self, venv: VarEnv) -> Hir<'cx> {
self.val.to_hir(venv)
}
- pub fn to_expr_tyenv(&self, tyenv: &TyEnv) -> Expr {
+ pub fn to_expr_tyenv(&self, tyenv: &TyEnv<'cx>) -> Expr {
self.val.to_hir(tyenv.as_varenv()).to_expr_tyenv(tyenv)
}
}
-impl<'hir> Tir<'hir> {
- pub fn from_hir(hir: &'hir Hir, ty: Type) -> Self {
+impl<'cx, 'hir> Tir<'cx, 'hir> {
+ pub fn from_hir(hir: &'hir Hir<'cx>, ty: Type<'cx>) -> Self {
Tir { hir, ty }
}
pub fn span(&self) -> Span {
self.as_hir().span()
}
- pub fn ty(&self) -> &Type {
+ pub fn ty(&self) -> &Type<'cx> {
&self.ty
}
- pub fn into_ty(self) -> Type {
+ pub fn into_ty(self) -> Type<'cx> {
self.ty
}
- pub fn to_hir(&self) -> Hir {
+ pub fn to_hir(&self) -> Hir<'cx> {
self.as_hir().clone()
}
- pub fn as_hir(&self) -> &Hir {
- &self.hir
+ pub fn as_hir(&self) -> &'hir Hir<'cx> {
+ self.hir
}
- pub fn to_expr_tyenv(&self, env: &TyEnv) -> Expr {
+ pub fn to_expr_tyenv(&self, env: &TyEnv<'cx>) -> Expr {
self.as_hir().to_expr_tyenv(env)
}
/// Eval the Tir. It will actually get evaluated only as needed on demand.
- pub fn eval(&self, env: impl Into<NzEnv>) -> Nir {
+ pub fn eval(&self, env: impl Into<NzEnv<'cx>>) -> Nir<'cx> {
self.as_hir().eval(env.into())
}
- pub fn ensure_is_type(&self, env: &TyEnv) -> Result<(), TypeError> {
+ pub fn ensure_is_type(&self, env: &TyEnv<'cx>) -> Result<(), TypeError> {
if self.ty().as_const().is_none() {
return mkerr(
ErrorBuilder::new(format!(
@@ -159,7 +160,10 @@ impl<'hir> Tir<'hir> {
Ok(())
}
/// Evaluate to a Type.
- pub fn eval_to_type(&self, env: &TyEnv) -> Result<Type, TypeError> {
+ pub fn eval_to_type(
+ &self,
+ env: &TyEnv<'cx>,
+ ) -> Result<Type<'cx>, TypeError> {
self.ensure_is_type(env)?;
Ok(Type::new(
self.eval(env),
diff --git a/dhall/src/semantics/tck/typecheck.rs b/dhall/src/semantics/tck/typecheck.rs
index 7e8c0e1..8218368 100644
--- a/dhall/src/semantics/tck/typecheck.rs
+++ b/dhall/src/semantics/tck/typecheck.rs
@@ -29,11 +29,12 @@ pub fn mk_span_err<T, S: ToString>(span: Span, msg: S) -> Result<T, TypeError> {
/// When all sub-expressions have been typed, check the remaining toplevel
/// layer.
-fn type_one_layer(
- env: &TyEnv<'_>,
- ekind: ExprKind<Tir<'_>>,
+fn type_one_layer<'cx>(
+ env: &TyEnv<'cx>,
+ ekind: ExprKind<Tir<'cx, '_>>,
span: Span,
-) -> Result<Type, TypeError> {
+) -> Result<Type<'cx>, TypeError> {
+ let cx = env.cx();
let span_err = |msg: &str| mk_span_err(span.clone(), msg);
Ok(match ekind {
@@ -51,18 +52,21 @@ fn type_one_layer(
ExprKind::Const(Const::Type) => Type::from_const(Const::Kind),
ExprKind::Const(Const::Kind) => Type::from_const(Const::Sort),
- ExprKind::Num(num) => Type::from_builtin(match num {
- NumKind::Bool(_) => Builtin::Bool,
- NumKind::Natural(_) => Builtin::Natural,
- NumKind::Integer(_) => Builtin::Integer,
- NumKind::Double(_) => Builtin::Double,
- }),
+ ExprKind::Num(num) => Type::from_builtin(
+ cx,
+ match num {
+ NumKind::Bool(_) => Builtin::Bool,
+ NumKind::Natural(_) => Builtin::Natural,
+ NumKind::Integer(_) => Builtin::Integer,
+ NumKind::Double(_) => Builtin::Double,
+ },
+ ),
ExprKind::Builtin(b) => {
let t_hir = type_of_builtin(b);
typecheck(env.cx(), &t_hir)?.eval_to_type(env)?
}
ExprKind::TextLit(interpolated) => {
- let text_type = Type::from_builtin(Builtin::Text);
+ let text_type = Type::from_builtin(cx, Builtin::Text);
for contents in interpolated.iter() {
use InterpolatedTextContents::Expr;
if let Expr(x) = contents {
@@ -79,7 +83,7 @@ fn type_one_layer(
}
let t = x.ty().to_nir();
- Nir::from_builtin(Builtin::Optional)
+ Nir::from_builtin(cx, Builtin::Optional)
.app(t)
.to_type(Const::Type)
}
@@ -104,7 +108,9 @@ fn type_one_layer(
}
let t = x.ty().to_nir();
- Nir::from_builtin(Builtin::List).app(t).to_type(Const::Type)
+ Nir::from_builtin(cx, Builtin::List)
+ .app(t)
+ .to_type(Const::Type)
}
ExprKind::RecordLit(kvs) => {
// An empty record type has type Type
@@ -171,11 +177,11 @@ fn type_one_layer(
/// to compare with.
// We pass the annotation to avoid duplicating the annot checking logic. I hope one day we can use
// it to handle the annotations in merge/toMap/etc. uniformly.
-pub fn type_with<'hir>(
- env: &TyEnv<'_>,
- hir: &'hir Hir,
- annot: Option<Type>,
-) -> Result<Tir<'hir>, TypeError> {
+pub fn type_with<'cx, 'hir>(
+ env: &TyEnv<'cx>,
+ hir: &'hir Hir<'cx>,
+ annot: Option<Type<'cx>>,
+) -> Result<Tir<'cx, 'hir>, TypeError> {
let tir = match hir.kind() {
HirKind::Var(var) => Tir::from_hir(hir, env.lookup(*var)),
HirKind::Import(_, ty) => Tir::from_hir(hir, ty.clone()),
@@ -268,19 +274,19 @@ pub fn type_with<'hir>(
/// Typecheck an expression and return the expression annotated with its type if type-checking
/// succeeded, or an error if type-checking failed.
-pub fn typecheck<'hir>(
- cx: Ctxt<'_>,
- hir: &'hir Hir,
-) -> Result<Tir<'hir>, TypeError> {
+pub fn typecheck<'cx, 'hir>(
+ cx: Ctxt<'cx>,
+ hir: &'hir Hir<'cx>,
+) -> Result<Tir<'cx, 'hir>, TypeError> {
type_with(&TyEnv::new(cx), hir, None)
}
/// Like `typecheck`, but additionally checks that the expression's type matches the provided type.
-pub fn typecheck_with<'hir>(
- cx: Ctxt<'_>,
- hir: &'hir Hir,
- ty: &Hir,
-) -> Result<Tir<'hir>, TypeError> {
+pub fn typecheck_with<'cx, 'hir>(
+ cx: Ctxt<'cx>,
+ hir: &'hir Hir<'cx>,
+ ty: &Hir<'cx>,
+) -> Result<Tir<'cx, 'hir>, TypeError> {
let ty = typecheck(cx, ty)?.eval_to_type(&TyEnv::new(cx))?;
type_with(&TyEnv::new(cx), hir, Some(ty))
}
generated by cgit v1.2.3 (git 2.25.1) at 2024-06-30 19:04:29 +0000