From 3a623acaf70c934ee9dbd74dfadcaa2c612160c5 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Sun, 6 Dec 2020 20:10:51 +0000 Subject: Make global store of imports and import results --- dhall/src/lib.rs | 3 +++ 1 file changed, 3 insertions(+) (limited to 'dhall/src/lib.rs') diff --git a/dhall/src/lib.rs b/dhall/src/lib.rs index 6747eff..d079e92 100644 --- a/dhall/src/lib.rs +++ b/dhall/src/lib.rs @@ -9,6 +9,7 @@ )] pub mod builtins; +pub mod ctxt; pub mod error; pub mod operations; pub mod semantics; @@ -26,6 +27,8 @@ use crate::semantics::resolve::ImportLocation; use crate::semantics::{typecheck, typecheck_with, Hir, Nir, Tir, Type}; use crate::syntax::Expr; +pub use ctxt::{Ctxt, ImportId, ImportResultId}; + #[derive(Debug, Clone)] pub struct Parsed(Expr, ImportLocation); -- cgit v1.2.3 From 6287b7a7f9e421877ee13fefa586395fec844c99 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Sun, 6 Dec 2020 21:41:03 +0000 Subject: Thread cx through typecheck --- dhall/src/lib.rs | 11 ++++++++--- 1 file changed, 8 insertions(+), 3 deletions(-) (limited to 'dhall/src/lib.rs') 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 { - resolve::resolve(self) + // TODO: thread cx + Ctxt::with_new(|cx| resolve::resolve(cx, self)) } pub fn skip_resolve(self) -> Result { resolve::skip_resolve(self) @@ -91,10 +92,14 @@ impl Parsed { impl Resolved { pub fn typecheck(&self) -> Result { - 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 { - 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 { -- cgit v1.2.3 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/lib.rs | 76 ++++++++++++++++++++++++++------------------------------ 1 file changed, 35 insertions(+), 41 deletions(-) (limited to 'dhall/src/lib.rs') diff --git a/dhall/src/lib.rs b/dhall/src/lib.rs index 661c33c..ec2b813 100644 --- a/dhall/src/lib.rs +++ b/dhall/src/lib.rs @@ -5,7 +5,8 @@ clippy::needless_lifetimes, clippy::new_ret_no_self, clippy::new_without_default, - clippy::useless_format + clippy::useless_format, + unreachable_code )] pub mod builtins; @@ -36,20 +37,20 @@ pub struct Parsed(Expr, ImportLocation); /// /// Invariant: there must be no `Import` nodes or `ImportAlt` operations left. #[derive(Debug, Clone)] -pub struct Resolved(Hir); +pub struct Resolved<'cx>(Hir<'cx>); /// A typed expression #[derive(Debug, Clone)] -pub struct Typed { - pub hir: Hir, - pub ty: Type, +pub struct Typed<'cx> { + pub hir: Hir<'cx>, + pub ty: Type<'cx>, } /// A normalized expression. /// /// This is actually a lie, because the expression will only get normalized on demand. #[derive(Debug, Clone)] -pub struct Normalized(Nir); +pub struct Normalized<'cx>(Nir<'cx>); /// Controls conversion from `Nir` to `Expr` #[derive(Copy, Clone, Default)] @@ -76,11 +77,10 @@ impl Parsed { parse::parse_binary(data) } - pub fn resolve(self) -> Result { - // TODO: thread cx - Ctxt::with_new(|cx| resolve::resolve(cx, self)) + pub fn resolve<'cx>(self, cx: Ctxt<'cx>) -> Result, Error> { + resolve::resolve(cx, self) } - pub fn skip_resolve(self) -> Result { + pub fn skip_resolve<'cx>(self) -> Result, Error> { resolve::skip_resolve(self) } @@ -90,16 +90,16 @@ impl Parsed { } } -impl Resolved { - pub fn typecheck(&self) -> Result { - // TODO: thread cx - Ctxt::with_new(|cx| Ok(Typed::from_tir(typecheck(cx, &self.0)?))) +impl<'cx> Resolved<'cx> { + pub fn typecheck(&self, cx: Ctxt<'cx>) -> Result, TypeError> { + Ok(Typed::from_tir(typecheck(cx, &self.0)?)) } - pub fn typecheck_with(self, ty: &Hir) -> Result { - // TODO: thread cx - Ctxt::with_new(|cx| { - Ok(Typed::from_tir(typecheck_with(cx, &self.0, ty)?)) - }) + pub fn typecheck_with( + self, + cx: Ctxt<'cx>, + ty: &Hir<'cx>, + ) -> Result, TypeError> { + 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 { @@ -107,16 +107,16 @@ impl Resolved { } } -impl Typed { - fn from_tir(tir: Tir<'_>) -> Self { +impl<'cx> Typed<'cx> { + fn from_tir(tir: Tir<'cx, '_>) -> Self { Typed { hir: tir.as_hir().clone(), ty: tir.ty().clone(), } } /// Reduce an expression to its normal form, performing beta reduction - pub fn normalize(&self) -> Normalized { - Normalized(self.hir.eval_closed_expr()) + pub fn normalize(&self, cx: Ctxt<'cx>) -> Normalized<'cx> { + Normalized(self.hir.eval_closed_expr(cx)) } /// Converts a value back to the corresponding AST expression. @@ -124,24 +124,24 @@ impl Typed { self.hir.to_expr(ToExprOptions { alpha: false }) } - pub fn ty(&self) -> &Type { + pub fn ty(&self) -> &Type<'cx> { &self.ty } - pub fn get_type(&self) -> Result { + pub fn get_type(&self) -> Result, TypeError> { Ok(Normalized(self.ty.clone().into_nir())) } } -impl Normalized { +impl<'cx> Normalized<'cx> { /// Converts a value back to the corresponding AST expression. pub fn to_expr(&self) -> Expr { self.0.to_expr(ToExprOptions::default()) } /// Converts a value back to the corresponding Hir expression. - pub fn to_hir(&self) -> Hir { + pub fn to_hir(&self) -> Hir<'cx> { self.0.to_hir_noenv() } - pub fn as_nir(&self) -> &Nir { + pub fn as_nir(&self) -> &Nir<'cx> { &self.0 } /// Converts a value back to the corresponding AST expression, alpha-normalizing in the process. @@ -178,37 +178,31 @@ impl From for Expr { other.to_expr() } } -impl From for Expr { - fn from(other: Normalized) -> Self { +impl<'cx> From> for Expr { + fn from(other: Normalized<'cx>) -> Self { other.to_expr() } } -impl Display for Resolved { +impl<'cx> Display for Resolved<'cx> { fn fmt(&self, f: &mut std::fmt::Formatter) -> Result<(), std::fmt::Error> { self.to_expr().fmt(f) } } -impl Eq for Typed {} -impl PartialEq for Typed { - fn eq(&self, other: &Self) -> bool { - self.normalize() == other.normalize() - } -} -impl Display for Typed { +impl<'cx> Display for Typed<'cx> { fn fmt(&self, f: &mut std::fmt::Formatter) -> Result<(), std::fmt::Error> { self.to_expr().fmt(f) } } -impl Eq for Normalized {} -impl PartialEq for Normalized { +impl<'cx> Eq for Normalized<'cx> {} +impl<'cx> PartialEq for Normalized<'cx> { fn eq(&self, other: &Self) -> bool { self.0 == other.0 } } -impl Display for Normalized { +impl<'cx> Display for Normalized<'cx> { fn fmt(&self, f: &mut std::fmt::Formatter) -> Result<(), std::fmt::Error> { self.to_expr().fmt(f) } -- cgit v1.2.3 From 8c5b3ff15f2125e9d731fc199e194e1993c36b37 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Mon, 7 Dec 2020 14:15:43 +0000 Subject: Thread cx everywhere else imports are read --- dhall/src/lib.rs | 42 +++++++++--------------------------------- 1 file changed, 9 insertions(+), 33 deletions(-) (limited to 'dhall/src/lib.rs') diff --git a/dhall/src/lib.rs b/dhall/src/lib.rs index ec2b813..7f77334 100644 --- a/dhall/src/lib.rs +++ b/dhall/src/lib.rs @@ -5,8 +5,7 @@ clippy::needless_lifetimes, clippy::new_ret_no_self, clippy::new_without_default, - clippy::useless_format, - unreachable_code + clippy::useless_format )] pub mod builtins; @@ -17,7 +16,6 @@ pub mod semantics; pub mod syntax; pub mod utils; -use std::fmt::Display; use std::path::Path; use url::Url; @@ -102,8 +100,8 @@ impl<'cx> Resolved<'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 { - self.0.to_expr_noopts() + pub fn to_expr(&self, cx: Ctxt<'cx>) -> Expr { + self.0.to_expr_noopts(cx) } } @@ -120,8 +118,8 @@ impl<'cx> Typed<'cx> { } /// Converts a value back to the corresponding AST expression. - fn to_expr(&self) -> Expr { - self.hir.to_expr(ToExprOptions { alpha: false }) + fn to_expr(&self, cx: Ctxt<'cx>) -> Expr { + self.hir.to_expr(cx, ToExprOptions { alpha: false }) } pub fn ty(&self) -> &Type<'cx> { @@ -134,8 +132,8 @@ impl<'cx> Typed<'cx> { impl<'cx> Normalized<'cx> { /// Converts a value back to the corresponding AST expression. - pub fn to_expr(&self) -> Expr { - self.0.to_expr(ToExprOptions::default()) + pub fn to_expr(&self, cx: Ctxt<'cx>) -> Expr { + self.0.to_expr(cx, ToExprOptions::default()) } /// Converts a value back to the corresponding Hir expression. pub fn to_hir(&self) -> Hir<'cx> { @@ -145,8 +143,8 @@ impl<'cx> Normalized<'cx> { &self.0 } /// Converts a value back to the corresponding AST expression, alpha-normalizing in the process. - pub fn to_expr_alpha(&self) -> Expr { - self.0.to_expr(ToExprOptions { alpha: true }) + pub fn to_expr_alpha(&self, cx: Ctxt<'cx>) -> Expr { + self.0.to_expr(cx, ToExprOptions { alpha: true }) } } @@ -178,23 +176,6 @@ impl From for Expr { other.to_expr() } } -impl<'cx> From> for Expr { - fn from(other: Normalized<'cx>) -> Self { - other.to_expr() - } -} - -impl<'cx> Display for Resolved<'cx> { - fn fmt(&self, f: &mut std::fmt::Formatter) -> Result<(), std::fmt::Error> { - self.to_expr().fmt(f) - } -} - -impl<'cx> Display for Typed<'cx> { - fn fmt(&self, f: &mut std::fmt::Formatter) -> Result<(), std::fmt::Error> { - self.to_expr().fmt(f) - } -} impl<'cx> Eq for Normalized<'cx> {} impl<'cx> PartialEq for Normalized<'cx> { @@ -202,8 +183,3 @@ impl<'cx> PartialEq for Normalized<'cx> { self.0 == other.0 } } -impl<'cx> Display for Normalized<'cx> { - fn fmt(&self, f: &mut std::fmt::Formatter) -> Result<(), std::fmt::Error> { - self.to_expr().fmt(f) - } -} -- cgit v1.2.3 From 922199ab322efa7b62bf4698cf5ed9e2d7a378c0 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Mon, 7 Dec 2020 15:24:36 +0000 Subject: Unify `skip_resolve_expr` with normal resolution --- dhall/src/lib.rs | 15 +++++++++++++-- 1 file changed, 13 insertions(+), 2 deletions(-) (limited to 'dhall/src/lib.rs') diff --git a/dhall/src/lib.rs b/dhall/src/lib.rs index 7f77334..c27b633 100644 --- a/dhall/src/lib.rs +++ b/dhall/src/lib.rs @@ -58,6 +58,11 @@ pub struct ToExprOptions { } impl Parsed { + /// Construct from an `Expr`. This `Expr` will have imports disabled. + pub fn from_expr_without_imports(e: Expr) -> Self { + Parsed(e, ImportLocation::dhall_code_without_imports()) + } + pub fn parse_file(f: &Path) -> Result { parse::parse_file(f) } @@ -78,8 +83,11 @@ impl Parsed { pub fn resolve<'cx>(self, cx: Ctxt<'cx>) -> Result, Error> { resolve::resolve(cx, self) } - pub fn skip_resolve<'cx>(self) -> Result, Error> { - resolve::skip_resolve(self) + pub fn skip_resolve<'cx>( + self, + cx: Ctxt<'cx>, + ) -> Result, Error> { + resolve::skip_resolve(cx, self) } /// Converts a value back to the corresponding AST expression. @@ -122,6 +130,9 @@ impl<'cx> Typed<'cx> { self.hir.to_expr(cx, ToExprOptions { alpha: false }) } + pub fn as_hir(&self) -> &Hir<'cx> { + &self.hir + } pub fn ty(&self) -> &Type<'cx> { &self.ty } -- cgit v1.2.3 From 4473f3549f331c51a7df0e307d356a06c00d7288 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Mon, 7 Dec 2020 19:02:07 +0000 Subject: Resolve imports and alternatives outside of the ast traversal --- dhall/src/lib.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'dhall/src/lib.rs') diff --git a/dhall/src/lib.rs b/dhall/src/lib.rs index c27b633..03d3931 100644 --- a/dhall/src/lib.rs +++ b/dhall/src/lib.rs @@ -26,7 +26,7 @@ use crate::semantics::resolve::ImportLocation; use crate::semantics::{typecheck, typecheck_with, Hir, Nir, Tir, Type}; use crate::syntax::Expr; -pub use ctxt::{Ctxt, ImportId, ImportResultId}; +pub use ctxt::*; #[derive(Debug, Clone)] pub struct Parsed(Expr, ImportLocation); -- cgit v1.2.3 From d0a61179addf838d33e7e7a4c6a13f06e871e9c5 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Mon, 7 Dec 2020 19:30:04 +0000 Subject: Soothe clippy --- dhall/src/lib.rs | 1 + 1 file changed, 1 insertion(+) (limited to 'dhall/src/lib.rs') diff --git a/dhall/src/lib.rs b/dhall/src/lib.rs index 03d3931..ad16a24 100644 --- a/dhall/src/lib.rs +++ b/dhall/src/lib.rs @@ -5,6 +5,7 @@ clippy::needless_lifetimes, clippy::new_ret_no_self, clippy::new_without_default, + clippy::try_err, clippy::useless_format )] -- cgit v1.2.3