diff options
author | Nadrieril | 2020-12-06 21:41:03 +0000 |
---|---|---|
committer | Nadrieril | 2020-12-07 19:34:38 +0000 |
commit | 6287b7a7f9e421877ee13fefa586395fec844c99 (patch) | |
tree | 65129001dbd7e56561df656dc8eee8f441a05b25 /dhall/src | |
parent | 9991bd4891774c4dd598decae02ee860554d2ab7 (diff) |
Thread cx through typecheck
Diffstat (limited to '')
-rw-r--r-- | dhall/src/builtins.rs | 16 | ||||
-rw-r--r-- | dhall/src/ctxt.rs | 8 | ||||
-rw-r--r-- | dhall/src/lib.rs | 11 | ||||
-rw-r--r-- | dhall/src/operations/typecheck.rs | 8 | ||||
-rw-r--r-- | dhall/src/semantics/resolve/hir.rs | 9 | ||||
-rw-r--r-- | dhall/src/semantics/resolve/resolve.rs | 6 | ||||
-rw-r--r-- | dhall/src/semantics/tck/env.rs | 16 | ||||
-rw-r--r-- | dhall/src/semantics/tck/typecheck.rs | 19 |
8 files changed, 65 insertions, 28 deletions
diff --git a/dhall/src/builtins.rs b/dhall/src/builtins.rs index cc426dd..f92f1c3 100644 --- a/dhall/src/builtins.rs +++ b/dhall/src/builtins.rs @@ -11,6 +11,7 @@ use crate::syntax::{ Const, Expr, ExprKind, InterpolatedText, InterpolatedTextContents, Label, NaiveDouble, NumKind, Span, UnspannedExpr, V, }; +use crate::Ctxt; /// Built-ins #[derive(Debug, Copy, Clone, PartialEq, Eq, Hash)] @@ -98,12 +99,14 @@ pub struct BuiltinClosure { impl BuiltinClosure { pub fn new(b: Builtin, env: NzEnv) -> NirKind { - apply_builtin(b, Vec::new(), env) + // TODO: thread cx + Ctxt::with_new(|cx| apply_builtin(cx, b, Vec::new(), env)) } pub fn apply(&self, a: Nir) -> NirKind { use std::iter::once; let args = self.args.iter().cloned().chain(once(a)).collect(); - apply_builtin(self.b, args, self.env.clone()) + // TODO: thread cx + Ctxt::with_new(|cx| apply_builtin(cx, self.b, args, self.env.clone())) } pub fn to_hirkind(&self, venv: VarEnv) -> HirKind { HirKind::Expr(self.args.iter().fold( @@ -307,7 +310,12 @@ macro_rules! make_closure { } #[allow(clippy::cognitive_complexity)] -fn apply_builtin(b: Builtin, args: Vec<Nir>, env: NzEnv) -> NirKind { +fn apply_builtin( + cx: Ctxt<'_>, + b: Builtin, + args: Vec<Nir>, + env: NzEnv, +) -> NirKind { use NirKind::*; use NumKind::{Bool, Double, Integer, Natural}; @@ -318,7 +326,7 @@ fn apply_builtin(b: Builtin, args: Vec<Nir>, env: NzEnv) -> NirKind { DoneAsIs, } let make_closure = |e| { - typecheck(&skip_resolve_expr(&e).unwrap()) + typecheck(cx, &skip_resolve_expr(&e).unwrap()) .unwrap() .eval(env.clone()) }; diff --git a/dhall/src/ctxt.rs b/dhall/src/ctxt.rs index 2394d8e..37fab35 100644 --- a/dhall/src/ctxt.rs +++ b/dhall/src/ctxt.rs @@ -108,3 +108,11 @@ impl<'cx> std::ops::Index<ImportResultId> for CtxtS<'cx> { &self.import_results[id.0] } } + +/// Empty impl, because `FrozenVec` does not implement `Debug` and I can't be bothered to do it +/// myself. +impl<'cx> std::fmt::Debug for Ctxt<'cx> { + fn fmt(&self, _: &mut std::fmt::Formatter) -> std::fmt::Result { + Ok(()) + } +} diff --git a/dhall/src/lib.rs b/dhall/src/lib.rs index d079e92..661c33c 100644 --- a/dhall/src/lib.rs +++ b/dhall/src/lib.rs @@ -77,7 +77,8 @@ impl Parsed { } pub fn resolve(self) -> Result<Resolved, Error> { - resolve::resolve(self) + // TODO: thread cx + Ctxt::with_new(|cx| resolve::resolve(cx, self)) } pub fn skip_resolve(self) -> Result<Resolved, Error> { resolve::skip_resolve(self) @@ -91,10 +92,14 @@ impl Parsed { impl Resolved { pub fn typecheck(&self) -> Result<Typed, TypeError> { - Ok(Typed::from_tir(typecheck(&self.0)?)) + // TODO: thread cx + Ctxt::with_new(|cx| Ok(Typed::from_tir(typecheck(cx, &self.0)?))) } pub fn typecheck_with(self, ty: &Hir) -> Result<Typed, TypeError> { - Ok(Typed::from_tir(typecheck_with(&self.0, ty)?)) + // TODO: thread cx + Ctxt::with_new(|cx| { + Ok(Typed::from_tir(typecheck_with(cx, &self.0, ty)?)) + }) } /// Converts a value back to the corresponding AST expression. pub fn to_expr(&self) -> Expr { diff --git a/dhall/src/operations/typecheck.rs b/dhall/src/operations/typecheck.rs index bc0e864..5718114 100644 --- a/dhall/src/operations/typecheck.rs +++ b/dhall/src/operations/typecheck.rs @@ -13,7 +13,7 @@ use crate::syntax::{Const, ExprKind, Span}; fn check_rectymerge( span: &Span, - env: &TyEnv, + env: &TyEnv<'_>, x: Nir, y: Nir, ) -> Result<(), TypeError> { @@ -45,7 +45,7 @@ fn check_rectymerge( } fn typecheck_binop( - env: &TyEnv, + env: &TyEnv<'_>, span: Span, op: BinOp, l: Tir<'_>, @@ -150,7 +150,7 @@ fn typecheck_binop( } fn typecheck_merge( - env: &TyEnv, + env: &TyEnv<'_>, span: Span, record: &Tir<'_>, scrut: &Tir<'_>, @@ -288,7 +288,7 @@ fn typecheck_merge( } pub fn typecheck_operation( - env: &TyEnv, + env: &TyEnv<'_>, span: Span, opkind: OpKind<Tir<'_>>, ) -> Result<Type, TypeError> { diff --git a/dhall/src/semantics/resolve/hir.rs b/dhall/src/semantics/resolve/hir.rs index 8869915..c2d1883 100644 --- a/dhall/src/semantics/resolve/hir.rs +++ b/dhall/src/semantics/resolve/hir.rs @@ -1,7 +1,7 @@ use crate::error::TypeError; use crate::semantics::{type_with, NameEnv, Nir, NzEnv, Tir, TyEnv, Type}; use crate::syntax::{Expr, ExprKind, Span, V}; -use crate::ToExprOptions; +use crate::{Ctxt, ToExprOptions}; /// Stores an alpha-normalized variable. #[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)] @@ -76,8 +76,11 @@ impl Hir { ) -> Result<Tir<'hir>, TypeError> { type_with(env, self, None) } - pub fn typecheck_noenv<'hir>(&'hir self) -> Result<Tir<'hir>, TypeError> { - self.typecheck(&TyEnv::new()) + pub fn typecheck_noenv<'hir>( + &'hir self, + cx: Ctxt<'_>, + ) -> Result<Tir<'hir>, TypeError> { + self.typecheck(&TyEnv::new(cx)) } /// Eval the Hir. It will actually get evaluated only as needed on demand. diff --git a/dhall/src/semantics/resolve/resolve.rs b/dhall/src/semantics/resolve/resolve.rs index 955e2fa..cf72f80 100644 --- a/dhall/src/semantics/resolve/resolve.rs +++ b/dhall/src/semantics/resolve/resolve.rs @@ -250,7 +250,7 @@ impl ImportLocation { ImportMode::Location => { let expr = self.kind.to_location(); let hir = skip_resolve_expr(&expr)?; - let ty = hir.typecheck_noenv()?.ty().clone(); + let ty = hir.typecheck_noenv(env.cx())?.ty().clone(); (hir, ty) } }; @@ -463,8 +463,8 @@ fn resolve_with_env<'cx>( Ok(Resolved(resolved)) } -pub fn resolve(parsed: Parsed) -> Result<Resolved, Error> { - Ctxt::with_new(|cx| resolve_with_env(&mut ImportEnv::new(cx), parsed)) +pub fn resolve(cx: Ctxt<'_>, parsed: Parsed) -> Result<Resolved, Error> { + resolve_with_env(&mut ImportEnv::new(cx), parsed) } pub fn skip_resolve_expr(expr: &Expr) -> Result<Hir, Error> { diff --git a/dhall/src/semantics/tck/env.rs b/dhall/src/semantics/tck/env.rs index 1fa66f0..fc0ce9f 100644 --- a/dhall/src/semantics/tck/env.rs +++ b/dhall/src/semantics/tck/env.rs @@ -1,5 +1,6 @@ use crate::semantics::{AlphaVar, NameEnv, Nir, NzEnv, NzVar, Type, ValEnv}; use crate::syntax::Label; +use crate::Ctxt; /// Environment for indexing variables. #[derive(Debug, Clone, Copy, Default)] @@ -9,7 +10,8 @@ pub struct VarEnv { /// Environment for typing expressions. #[derive(Debug, Clone)] -pub struct TyEnv { +pub struct TyEnv<'cx> { + cx: Ctxt<'cx>, names: NameEnv, items: ValEnv<Type>, } @@ -38,13 +40,17 @@ impl VarEnv { } } -impl TyEnv { - pub fn new() -> Self { +impl<'cx> TyEnv<'cx> { + pub fn new(cx: Ctxt<'cx>) -> Self { TyEnv { + cx, names: NameEnv::new(), items: ValEnv::new(), } } + pub fn cx(&self) -> Ctxt<'cx> { + self.cx + } pub fn as_varenv(&self) -> VarEnv { self.names.as_varenv() } @@ -57,12 +63,14 @@ impl TyEnv { pub fn insert_type(&self, x: &Label, ty: Type) -> 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 { TyEnv { + cx: self.cx, names: self.names.insert(x), items: self.items.insert_value(e, ty), } @@ -72,7 +80,7 @@ impl TyEnv { } } -impl<'a> From<&'a TyEnv> for NzEnv { +impl<'a, 'cx> From<&'a TyEnv<'cx>> for NzEnv { fn from(x: &'a TyEnv) -> Self { x.to_nzenv() } diff --git a/dhall/src/semantics/tck/typecheck.rs b/dhall/src/semantics/tck/typecheck.rs index 498bd76..7e8c0e1 100644 --- a/dhall/src/semantics/tck/typecheck.rs +++ b/dhall/src/semantics/tck/typecheck.rs @@ -5,6 +5,7 @@ use crate::error::{ErrorBuilder, TypeError, TypeMessage}; use crate::operations::typecheck_operation; use crate::semantics::{Hir, HirKind, Nir, NirKind, Tir, TyEnv, Type}; use crate::syntax::{Const, ExprKind, InterpolatedTextContents, NumKind, Span}; +use crate::Ctxt; fn function_check(a: Const, b: Const) -> Const { if b == Const::Type { @@ -29,7 +30,7 @@ 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, + env: &TyEnv<'_>, ekind: ExprKind<Tir<'_>>, span: Span, ) -> Result<Type, TypeError> { @@ -58,7 +59,7 @@ fn type_one_layer( }), ExprKind::Builtin(b) => { let t_hir = type_of_builtin(b); - typecheck(&t_hir)?.eval_to_type(env)? + typecheck(env.cx(), &t_hir)?.eval_to_type(env)? } ExprKind::TextLit(interpolated) => { let text_type = Type::from_builtin(Builtin::Text); @@ -171,7 +172,7 @@ fn type_one_layer( // 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, + env: &TyEnv<'_>, hir: &'hir Hir, annot: Option<Type>, ) -> Result<Tir<'hir>, TypeError> { @@ -267,15 +268,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>(hir: &'hir Hir) -> Result<Tir<'hir>, TypeError> { - type_with(&TyEnv::new(), hir, None) +pub fn typecheck<'hir>( + cx: Ctxt<'_>, + hir: &'hir Hir, +) -> Result<Tir<'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> { - let ty = typecheck(ty)?.eval_to_type(&TyEnv::new())?; - type_with(&TyEnv::new(), hir, Some(ty)) + let ty = typecheck(cx, ty)?.eval_to_type(&TyEnv::new(cx))?; + type_with(&TyEnv::new(cx), hir, Some(ty)) } |