From c785b7c0c6cd8b3b1cc15eb79caf982a757020ba Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Sun, 6 Dec 2020 23:55:21 +0000 Subject: Thread cx through normalization --- dhall/src/semantics/tck/env.rs | 16 +++++----- dhall/src/semantics/tck/tir.rs | 60 +++++++++++++++++++----------------- dhall/src/semantics/tck/typecheck.rs | 60 ++++++++++++++++++++---------------- 3 files changed, 73 insertions(+), 63 deletions(-) (limited to 'dhall/src/semantics/tck') 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, + 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 { 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 { 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) -> Nir { + pub fn eval(&self, env: impl Into>) -> 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 { + pub fn eval_to_type( + &self, + env: &TyEnv<'cx>, + ) -> Result, 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(span: Span, msg: S) -> Result { /// When all sub-expressions have been typed, check the remaining toplevel /// layer. -fn type_one_layer( - env: &TyEnv<'_>, - ekind: ExprKind>, +fn type_one_layer<'cx>( + env: &TyEnv<'cx>, + ekind: ExprKind>, span: Span, -) -> Result { +) -> Result, 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, -) -> Result, TypeError> { +pub fn type_with<'cx, 'hir>( + env: &TyEnv<'cx>, + hir: &'hir Hir<'cx>, + annot: Option>, +) -> Result, 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, TypeError> { +pub fn typecheck<'cx, 'hir>( + cx: Ctxt<'cx>, + hir: &'hir Hir<'cx>, +) -> Result, 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, TypeError> { +pub fn typecheck_with<'cx, 'hir>( + cx: Ctxt<'cx>, + hir: &'hir Hir<'cx>, + ty: &Hir<'cx>, +) -> Result, TypeError> { let ty = typecheck(cx, ty)?.eval_to_type(&TyEnv::new(cx))?; type_with(&TyEnv::new(cx), hir, Some(ty)) } -- cgit v1.2.3