From 5870a46d5ab5810901198f03ed461d5c3bb5aa8a Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Thu, 6 Feb 2020 17:58:48 +0000 Subject: Remove move type propagation through Value --- dhall/src/lib.rs | 32 ++++++++++---------------------- 1 file changed, 10 insertions(+), 22 deletions(-) (limited to 'dhall/src/lib.rs') diff --git a/dhall/src/lib.rs b/dhall/src/lib.rs index d8eeb4a..48d4d96 100644 --- a/dhall/src/lib.rs +++ b/dhall/src/lib.rs @@ -24,7 +24,7 @@ use crate::semantics::resolve; use crate::semantics::resolve::ImportRoot; use crate::semantics::{typecheck, typecheck_with, TyExpr, Value, ValueKind}; use crate::syntax::binary; -use crate::syntax::{Builtin, Const, Expr}; +use crate::syntax::{Builtin, Expr}; pub type ParsedExpr = Expr; pub type DecodedExpr = Expr; @@ -148,18 +148,12 @@ impl Normalized { self.0 } - pub(crate) fn from_const(c: Const) -> Self { - Normalized(Value::from_const(c)) - } - pub(crate) fn from_kind_and_type(v: ValueKind, t: Normalized) -> Self { - Normalized(Value::from_kind_and_type(v, t.into_value())) + pub(crate) fn from_kind(v: ValueKind) -> Self { + Normalized(Value::from_kind(v)) } pub(crate) fn from_value(th: Value) -> Self { Normalized(th) } - pub(crate) fn const_type() -> Self { - Normalized::from_const(Const::Type) - } pub fn make_builtin_type(b: Builtin) -> Self { Normalized::from_value(Value::from_builtin(b)) @@ -177,23 +171,17 @@ impl Normalized { pub fn make_record_type( kts: impl Iterator, ) -> Self { - Normalized::from_kind_and_type( - ValueKind::RecordType( - kts.map(|(k, t)| (k.into(), t.into_value())).collect(), - ), - Normalized::const_type(), - ) + Normalized::from_kind(ValueKind::RecordType( + kts.map(|(k, t)| (k.into(), t.into_value())).collect(), + )) } pub fn make_union_type( kts: impl Iterator)>, ) -> Self { - Normalized::from_kind_and_type( - ValueKind::UnionType( - kts.map(|(k, t)| (k.into(), t.map(|t| t.into_value()))) - .collect(), - ), - Normalized::const_type(), - ) + Normalized::from_kind(ValueKind::UnionType( + kts.map(|(k, t)| (k.into(), t.map(|t| t.into_value()))) + .collect(), + )) } } -- cgit v1.2.3 From a709c65eb28f1b6a666f15bfc2255da7bc7105ab Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Sun, 9 Feb 2020 21:38:37 +0000 Subject: Resolve variables alongside import resolution --- dhall/src/lib.rs | 25 ++++++++++++++++--------- 1 file changed, 16 insertions(+), 9 deletions(-) (limited to 'dhall/src/lib.rs') diff --git a/dhall/src/lib.rs b/dhall/src/lib.rs index 48d4d96..c2a2f19 100644 --- a/dhall/src/lib.rs +++ b/dhall/src/lib.rs @@ -18,11 +18,13 @@ pub mod syntax; use std::fmt::Display; use std::path::Path; -use crate::error::{EncodeError, Error, ImportError, TypeError}; +use crate::error::{EncodeError, Error, TypeError}; use crate::semantics::parse; use crate::semantics::resolve; use crate::semantics::resolve::ImportRoot; -use crate::semantics::{typecheck, typecheck_with, TyExpr, Value, ValueKind}; +use crate::semantics::{ + typecheck, typecheck_with, Hir, TyExpr, Value, ValueKind, +}; use crate::syntax::binary; use crate::syntax::{Builtin, Expr}; @@ -38,7 +40,7 @@ pub struct Parsed(ParsedExpr, ImportRoot); /// /// Invariant: there must be no `Import` nodes or `ImportAlt` operations left. #[derive(Debug, Clone)] -pub struct Resolved(ResolvedExpr); +pub struct Resolved(Hir); /// A typed expression #[derive(Debug, Clone)] @@ -73,10 +75,10 @@ impl Parsed { parse::parse_binary(data) } - pub fn resolve(self) -> Result { + pub fn resolve(self) -> Result { resolve::resolve(self) } - pub fn skip_resolve(self) -> Result { + pub fn skip_resolve(self) -> Result { resolve::skip_resolve_expr(self) } @@ -92,14 +94,14 @@ impl Parsed { impl Resolved { pub fn typecheck(&self) -> Result { - Ok(Typed(typecheck(&self.0)?)) + Ok(Typed(typecheck(&self.to_expr())?)) } pub fn typecheck_with(self, ty: &Normalized) -> Result { - Ok(Typed(typecheck_with(&self.0, ty.to_expr())?)) + Ok(Typed(typecheck_with(&self.to_expr(), ty.to_expr())?)) } /// Converts a value back to the corresponding AST expression. pub fn to_expr(&self) -> ResolvedExpr { - self.0.clone() + self.0.to_expr_noopts() } } @@ -207,7 +209,6 @@ macro_rules! derive_traits_for_wrapper_struct { } derive_traits_for_wrapper_struct!(Parsed); -derive_traits_for_wrapper_struct!(Resolved); impl std::hash::Hash for Normalized { fn hash(&self, state: &mut H) @@ -231,6 +232,12 @@ impl From for NormalizedExpr { } } +impl Display for Resolved { + 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 { -- cgit v1.2.3 From 21db63d3e614554f258526182c7ed89a2c244b65 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Sun, 9 Feb 2020 21:58:28 +0000 Subject: Take Hir for typecheck --- dhall/src/lib.rs | 10 +++++++--- 1 file changed, 7 insertions(+), 3 deletions(-) (limited to 'dhall/src/lib.rs') diff --git a/dhall/src/lib.rs b/dhall/src/lib.rs index c2a2f19..2d261f9 100644 --- a/dhall/src/lib.rs +++ b/dhall/src/lib.rs @@ -79,7 +79,7 @@ impl Parsed { resolve::resolve(self) } pub fn skip_resolve(self) -> Result { - resolve::skip_resolve_expr(self) + Ok(Resolved(resolve::skip_resolve(&self.0)?)) } pub fn encode(&self) -> Result, EncodeError> { @@ -94,10 +94,10 @@ impl Parsed { impl Resolved { pub fn typecheck(&self) -> Result { - Ok(Typed(typecheck(&self.to_expr())?)) + Ok(Typed(typecheck(&self.0)?)) } pub fn typecheck_with(self, ty: &Normalized) -> Result { - Ok(Typed(typecheck_with(&self.to_expr(), ty.to_expr())?)) + Ok(Typed(typecheck_with(&self.0, ty.to_hir())?)) } /// Converts a value back to the corresponding AST expression. pub fn to_expr(&self) -> ResolvedExpr { @@ -136,6 +136,10 @@ impl Normalized { normalize: false, }) } + /// Converts a value back to the corresponding Hir expression. + pub(crate) fn to_hir(&self) -> Hir { + self.0.to_hir_noenv() + } /// Converts a value back to the corresponding AST expression, alpha-normalizing in the process. pub(crate) fn to_expr_alpha(&self) -> NormalizedExpr { self.0.to_expr(ToExprOptions { -- cgit v1.2.3 From 5a2538d174fd36a8ed7f4fa344b9583fc48bd977 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Tue, 11 Feb 2020 13:12:13 +0000 Subject: Remove the Embed variant from ExprKind --- dhall/src/lib.rs | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) (limited to 'dhall/src/lib.rs') diff --git a/dhall/src/lib.rs b/dhall/src/lib.rs index 2d261f9..2f0ed4b 100644 --- a/dhall/src/lib.rs +++ b/dhall/src/lib.rs @@ -28,10 +28,10 @@ use crate::semantics::{ use crate::syntax::binary; use crate::syntax::{Builtin, Expr}; -pub type ParsedExpr = Expr; -pub type DecodedExpr = Expr; -pub type ResolvedExpr = Expr; -pub type NormalizedExpr = Expr; +pub type ParsedExpr = Expr; +pub type DecodedExpr = Expr; +pub type ResolvedExpr = Expr; +pub type NormalizedExpr = Expr; #[derive(Debug, Clone)] pub struct Parsed(ParsedExpr, ImportRoot); -- cgit v1.2.3 From 350d1cf7d9c114b1334b2743071b0b99ea64c1ec Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Thu, 13 Feb 2020 20:56:38 +0000 Subject: TyExpr always carries a type --- 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 2f0ed4b..ad54c9f 100644 --- a/dhall/src/lib.rs +++ b/dhall/src/lib.rs @@ -120,7 +120,7 @@ impl Typed { } pub(crate) fn get_type(&self) -> Result { - Ok(Normalized(self.0.get_type()?)) + Ok(Normalized(self.0.ty().clone())) } } -- cgit v1.2.3 From aa867b21f57f9bef2ec2b9d8450736f9111189ee Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Sat, 15 Feb 2020 19:44:40 +0000 Subject: Introduce proper Type struct --- 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 ad54c9f..144cac5 100644 --- a/dhall/src/lib.rs +++ b/dhall/src/lib.rs @@ -120,7 +120,7 @@ impl Typed { } pub(crate) fn get_type(&self) -> Result { - Ok(Normalized(self.0.ty().clone())) + Ok(Normalized(self.0.ty().clone().into_value())) } } -- cgit v1.2.3 From 2f65c02a995f6b6d4c755197fc074782f6bb100d Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Mon, 17 Feb 2020 18:12:44 +0000 Subject: Rename TyExpr to Tir --- dhall/src/lib.rs | 6 ++---- 1 file changed, 2 insertions(+), 4 deletions(-) (limited to 'dhall/src/lib.rs') diff --git a/dhall/src/lib.rs b/dhall/src/lib.rs index 144cac5..3fbc251 100644 --- a/dhall/src/lib.rs +++ b/dhall/src/lib.rs @@ -22,9 +22,7 @@ use crate::error::{EncodeError, Error, TypeError}; use crate::semantics::parse; use crate::semantics::resolve; use crate::semantics::resolve::ImportRoot; -use crate::semantics::{ - typecheck, typecheck_with, Hir, TyExpr, Value, ValueKind, -}; +use crate::semantics::{typecheck, typecheck_with, Hir, Tir, Value, ValueKind}; use crate::syntax::binary; use crate::syntax::{Builtin, Expr}; @@ -44,7 +42,7 @@ pub struct Resolved(Hir); /// A typed expression #[derive(Debug, Clone)] -pub struct Typed(TyExpr); +pub struct Typed(Tir); /// A normalized expression. /// -- cgit v1.2.3 From cd5e172002ce724be7bdd52883e121efa8817f20 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Mon, 17 Feb 2020 18:22:06 +0000 Subject: Rename Value to Nir --- dhall/src/lib.rs | 36 +++++++++++++++++------------------- 1 file changed, 17 insertions(+), 19 deletions(-) (limited to 'dhall/src/lib.rs') diff --git a/dhall/src/lib.rs b/dhall/src/lib.rs index 3fbc251..a4987c6 100644 --- a/dhall/src/lib.rs +++ b/dhall/src/lib.rs @@ -22,7 +22,7 @@ use crate::error::{EncodeError, Error, TypeError}; use crate::semantics::parse; use crate::semantics::resolve; use crate::semantics::resolve::ImportRoot; -use crate::semantics::{typecheck, typecheck_with, Hir, Tir, Value, ValueKind}; +use crate::semantics::{typecheck, typecheck_with, Hir, Nir, NirKind, Tir}; use crate::syntax::binary; use crate::syntax::{Builtin, Expr}; @@ -48,9 +48,9 @@ pub struct Typed(Tir); /// /// Invariant: the contained Typed expression must be in normal form, #[derive(Debug, Clone)] -pub struct Normalized(Value); +pub struct Normalized(Nir); -/// Controls conversion from `Value` to `Expr` +/// Controls conversion from `Nir` to `Expr` #[derive(Copy, Clone)] pub(crate) struct ToExprOptions { /// Whether to convert all variables to `_` @@ -118,7 +118,7 @@ impl Typed { } pub(crate) fn get_type(&self) -> Result { - Ok(Normalized(self.0.ty().clone().into_value())) + Ok(Normalized(self.0.ty().clone().into_nir())) } } @@ -145,45 +145,43 @@ impl Normalized { normalize: false, }) } - pub(crate) fn to_value(&self) -> Value { + pub(crate) fn to_nir(&self) -> Nir { self.0.clone() } - pub(crate) fn into_value(self) -> Value { + pub(crate) fn into_nir(self) -> Nir { self.0 } - pub(crate) fn from_kind(v: ValueKind) -> Self { - Normalized(Value::from_kind(v)) + pub(crate) fn from_kind(v: NirKind) -> Self { + Normalized(Nir::from_kind(v)) } - pub(crate) fn from_value(th: Value) -> Self { + pub(crate) fn from_nir(th: Nir) -> Self { Normalized(th) } pub fn make_builtin_type(b: Builtin) -> Self { - Normalized::from_value(Value::from_builtin(b)) + Normalized::from_nir(Nir::from_builtin(b)) } pub fn make_optional_type(t: Normalized) -> Self { - Normalized::from_value( - Value::from_builtin(Builtin::Optional).app(t.to_value()), + Normalized::from_nir( + Nir::from_builtin(Builtin::Optional).app(t.to_nir()), ) } pub fn make_list_type(t: Normalized) -> Self { - Normalized::from_value( - Value::from_builtin(Builtin::List).app(t.to_value()), - ) + Normalized::from_nir(Nir::from_builtin(Builtin::List).app(t.to_nir())) } pub fn make_record_type( kts: impl Iterator, ) -> Self { - Normalized::from_kind(ValueKind::RecordType( - kts.map(|(k, t)| (k.into(), t.into_value())).collect(), + Normalized::from_kind(NirKind::RecordType( + kts.map(|(k, t)| (k.into(), t.into_nir())).collect(), )) } pub fn make_union_type( kts: impl Iterator)>, ) -> Self { - Normalized::from_kind(ValueKind::UnionType( - kts.map(|(k, t)| (k.into(), t.map(|t| t.into_value()))) + Normalized::from_kind(NirKind::UnionType( + kts.map(|(k, t)| (k.into(), t.map(|t| t.into_nir()))) .collect(), )) } -- cgit v1.2.3 From ebe43bd6f1fd6feb1564ab9837399de7808b67b5 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Tue, 18 Feb 2020 18:39:10 +0000 Subject: Borrow relevant Hir from Tir --- dhall/src/lib.rs | 25 ++++++++++++++++++------- 1 file changed, 18 insertions(+), 7 deletions(-) (limited to 'dhall/src/lib.rs') diff --git a/dhall/src/lib.rs b/dhall/src/lib.rs index a4987c6..c329c66 100644 --- a/dhall/src/lib.rs +++ b/dhall/src/lib.rs @@ -22,7 +22,9 @@ use crate::error::{EncodeError, Error, TypeError}; use crate::semantics::parse; use crate::semantics::resolve; use crate::semantics::resolve::ImportRoot; -use crate::semantics::{typecheck, typecheck_with, Hir, Nir, NirKind, Tir}; +use crate::semantics::{ + typecheck, typecheck_with, Hir, Nir, NirKind, Tir, Type, +}; use crate::syntax::binary; use crate::syntax::{Builtin, Expr}; @@ -42,7 +44,10 @@ pub struct Resolved(Hir); /// A typed expression #[derive(Debug, Clone)] -pub struct Typed(Tir); +pub struct Typed { + hir: Hir, + ty: Type, +} /// A normalized expression. /// @@ -92,10 +97,10 @@ impl Parsed { impl Resolved { pub fn typecheck(&self) -> Result { - Ok(Typed(typecheck(&self.0)?)) + Ok(Typed::from_tir(typecheck(&self.0)?)) } pub fn typecheck_with(self, ty: &Normalized) -> Result { - Ok(Typed(typecheck_with(&self.0, ty.to_hir())?)) + Ok(Typed::from_tir(typecheck_with(&self.0, ty.to_hir())?)) } /// Converts a value back to the corresponding AST expression. pub fn to_expr(&self) -> ResolvedExpr { @@ -104,21 +109,27 @@ impl Resolved { } impl Typed { + fn from_tir(tir: Tir<'_>) -> 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.0.rec_eval_closed_expr()) + Normalized(self.hir.rec_eval_closed_expr()) } /// Converts a value back to the corresponding AST expression. fn to_expr(&self) -> ResolvedExpr { - self.0.to_expr(ToExprOptions { + self.hir.to_expr(ToExprOptions { alpha: false, normalize: false, }) } pub(crate) fn get_type(&self) -> Result { - Ok(Normalized(self.0.ty().clone().into_nir())) + Ok(Normalized(self.ty.clone().into_nir())) } } -- cgit v1.2.3 From 50a9dc4b9af19a35a983fe17108453d1d82d80ed Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Tue, 18 Feb 2020 18:46:26 +0000 Subject: Remove useless `normalize` option from ToExprOptions --- dhall/src/lib.rs | 19 ++++--------------- 1 file changed, 4 insertions(+), 15 deletions(-) (limited to 'dhall/src/lib.rs') diff --git a/dhall/src/lib.rs b/dhall/src/lib.rs index c329c66..c2f5020 100644 --- a/dhall/src/lib.rs +++ b/dhall/src/lib.rs @@ -51,7 +51,7 @@ pub struct Typed { /// A normalized expression. /// -/// Invariant: the contained Typed expression must be in normal form, +/// Invariant: the contained expression must be in normal form, #[derive(Debug, Clone)] pub struct Normalized(Nir); @@ -60,8 +60,6 @@ pub struct Normalized(Nir); pub(crate) struct ToExprOptions { /// Whether to convert all variables to `_` pub(crate) alpha: bool, - /// Whether to normalize before converting - pub(crate) normalize: bool, } impl Parsed { @@ -122,10 +120,7 @@ impl Typed { /// Converts a value back to the corresponding AST expression. fn to_expr(&self) -> ResolvedExpr { - self.hir.to_expr(ToExprOptions { - alpha: false, - normalize: false, - }) + self.hir.to_expr(ToExprOptions { alpha: false }) } pub(crate) fn get_type(&self) -> Result { @@ -140,10 +135,7 @@ impl Normalized { /// Converts a value back to the corresponding AST expression. pub fn to_expr(&self) -> NormalizedExpr { - self.0.to_expr(ToExprOptions { - alpha: false, - normalize: false, - }) + self.0.to_expr(ToExprOptions { alpha: false }) } /// Converts a value back to the corresponding Hir expression. pub(crate) fn to_hir(&self) -> Hir { @@ -151,10 +143,7 @@ impl Normalized { } /// Converts a value back to the corresponding AST expression, alpha-normalizing in the process. pub(crate) fn to_expr_alpha(&self) -> NormalizedExpr { - self.0.to_expr(ToExprOptions { - alpha: true, - normalize: false, - }) + self.0.to_expr(ToExprOptions { alpha: true }) } pub(crate) fn to_nir(&self) -> Nir { self.0.clone() -- cgit v1.2.3 From 7cbfc1a0d32766a383d1f48902502adaa2234d2f Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Tue, 18 Feb 2020 19:12:31 +0000 Subject: Avoid re-typechecking after import --- 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 c2f5020..9922144 100644 --- a/dhall/src/lib.rs +++ b/dhall/src/lib.rs @@ -123,6 +123,9 @@ impl Typed { self.hir.to_expr(ToExprOptions { alpha: false }) } + pub(crate) fn ty(&self) -> &Type { + &self.ty + } pub(crate) fn get_type(&self) -> Result { Ok(Normalized(self.ty.clone().into_nir())) } -- cgit v1.2.3