From 8edbeadbd0dc06a75ffb8bf3b0a54a62e3acc5fc Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Fri, 27 Dec 2019 14:26:40 +0000 Subject: Parameterize ValueKind by its subnodes --- dhall/src/semantics/phase/mod.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'dhall/src/semantics/phase/mod.rs') diff --git a/dhall/src/semantics/phase/mod.rs b/dhall/src/semantics/phase/mod.rs index 5332eb3..104a1ba 100644 --- a/dhall/src/semantics/phase/mod.rs +++ b/dhall/src/semantics/phase/mod.rs @@ -94,7 +94,7 @@ impl Typed { pub(crate) fn from_const(c: Const) -> Self { Typed(Value::from_const(c)) } - pub(crate) fn from_kind_and_type(v: ValueKind, t: Typed) -> Self { + pub(crate) fn from_kind_and_type(v: ValueKind, t: Typed) -> Self { Typed(Value::from_kind_and_type(v, t.into_value())) } pub(crate) fn from_value(th: Value) -> Self { -- cgit v1.2.3 From a030560e60c4ff1c724216f4a5640722eb89b227 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Fri, 27 Dec 2019 21:38:34 +0000 Subject: Use binder ids to reconstruct variables in expr output --- dhall/src/semantics/phase/mod.rs | 8 +------- 1 file changed, 1 insertion(+), 7 deletions(-) (limited to 'dhall/src/semantics/phase/mod.rs') diff --git a/dhall/src/semantics/phase/mod.rs b/dhall/src/semantics/phase/mod.rs index 104a1ba..5d17338 100644 --- a/dhall/src/semantics/phase/mod.rs +++ b/dhall/src/semantics/phase/mod.rs @@ -4,7 +4,7 @@ use std::path::Path; use crate::error::{EncodeError, Error, ImportError, TypeError}; use crate::semantics::core::value::Value; use crate::semantics::core::value::ValueKind; -use crate::semantics::core::var::{AlphaVar, Shift, Subst}; +use crate::semantics::core::var::{AlphaVar, Shift}; use crate::semantics::to_expr::ToExprOptions; use crate::syntax::binary; use crate::syntax::{Builtin, Const, Expr}; @@ -203,12 +203,6 @@ impl Shift for Normalized { } } -impl Subst for Typed { - fn subst_shift(&self, var: &AlphaVar, val: &Value) -> Self { - Typed(self.0.subst_shift(var, val)) - } -} - macro_rules! derive_traits_for_wrapper_struct { ($ty:ident) => { impl std::cmp::PartialEq for $ty { -- cgit v1.2.3 From 72d1e3c339cf550fa5af9981af6078a813feb80a Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Fri, 17 Jan 2020 11:03:40 +0000 Subject: Remove Shift/Subst traits --- dhall/src/semantics/phase/mod.rs | 13 ------------- 1 file changed, 13 deletions(-) (limited to 'dhall/src/semantics/phase/mod.rs') diff --git a/dhall/src/semantics/phase/mod.rs b/dhall/src/semantics/phase/mod.rs index 5d17338..6afed88 100644 --- a/dhall/src/semantics/phase/mod.rs +++ b/dhall/src/semantics/phase/mod.rs @@ -4,7 +4,6 @@ use std::path::Path; use crate::error::{EncodeError, Error, ImportError, TypeError}; use crate::semantics::core::value::Value; use crate::semantics::core::value::ValueKind; -use crate::semantics::core::var::{AlphaVar, Shift}; use crate::semantics::to_expr::ToExprOptions; use crate::syntax::binary; use crate::syntax::{Builtin, Const, Expr}; @@ -191,18 +190,6 @@ impl Normalized { } } -impl Shift for Typed { - fn shift(&self, delta: isize, var: &AlphaVar) -> Option { - Some(Typed(self.0.shift(delta, var)?)) - } -} - -impl Shift for Normalized { - fn shift(&self, delta: isize, var: &AlphaVar) -> Option { - Some(Normalized(self.0.shift(delta, var)?)) - } -} - macro_rules! derive_traits_for_wrapper_struct { ($ty:ident) => { impl std::cmp::PartialEq for $ty { -- cgit v1.2.3 From ec28905d32c23109da17696faefab284fde3e103 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Sat, 18 Jan 2020 18:46:09 +0000 Subject: Introduce intermediate representation that stores typed expr --- dhall/src/semantics/phase/mod.rs | 10 +++++++++- 1 file changed, 9 insertions(+), 1 deletion(-) (limited to 'dhall/src/semantics/phase/mod.rs') diff --git a/dhall/src/semantics/phase/mod.rs b/dhall/src/semantics/phase/mod.rs index 6afed88..4dc91e7 100644 --- a/dhall/src/semantics/phase/mod.rs +++ b/dhall/src/semantics/phase/mod.rs @@ -4,7 +4,6 @@ use std::path::Path; use crate::error::{EncodeError, Error, ImportError, TypeError}; use crate::semantics::core::value::Value; use crate::semantics::core::value::ValueKind; -use crate::semantics::to_expr::ToExprOptions; use crate::syntax::binary; use crate::syntax::{Builtin, Const, Expr}; use resolve::ImportRoot; @@ -38,6 +37,15 @@ pub struct Typed(Value); #[derive(Debug, Clone)] pub struct Normalized(Typed); +/// Controls conversion from `Value` to `Expr` +#[derive(Copy, Clone)] +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 { pub fn parse_file(f: &Path) -> Result { parse::parse_file(f) -- cgit v1.2.3 From 5a835d9db35bf76858e178e1bd66e60128879629 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Mon, 27 Jan 2020 18:45:09 +0000 Subject: Fix a bunch of bugs and more tck --- dhall/src/semantics/phase/mod.rs | 5 +++++ 1 file changed, 5 insertions(+) (limited to 'dhall/src/semantics/phase/mod.rs') diff --git a/dhall/src/semantics/phase/mod.rs b/dhall/src/semantics/phase/mod.rs index 4dc91e7..67cdc91 100644 --- a/dhall/src/semantics/phase/mod.rs +++ b/dhall/src/semantics/phase/mod.rs @@ -89,6 +89,11 @@ impl Resolved { pub fn to_expr(&self) -> ResolvedExpr { self.0.clone() } + pub fn tck_and_normalize_new_flow(&self) -> Result { + let val = crate::semantics::tck::typecheck::typecheck(&self.0)? + .normalize_whnf_noenv(); + Ok(Normalized(Typed(val))) + } } impl Typed { -- cgit v1.2.3 From f88880004c7dcf5e67c4d5e2330e6e879523f27b Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Wed, 29 Jan 2020 18:30:12 +0000 Subject: Use Normalized in serde_dhall --- dhall/src/semantics/phase/mod.rs | 126 +++++++++++++++++++++++---------------- 1 file changed, 74 insertions(+), 52 deletions(-) (limited to 'dhall/src/semantics/phase/mod.rs') diff --git a/dhall/src/semantics/phase/mod.rs b/dhall/src/semantics/phase/mod.rs index 67cdc91..68c32b2 100644 --- a/dhall/src/semantics/phase/mod.rs +++ b/dhall/src/semantics/phase/mod.rs @@ -35,7 +35,7 @@ pub struct Typed(Value); /// /// Invariant: the contained Typed expression must be in normal form, #[derive(Debug, Clone)] -pub struct Normalized(Typed); +pub struct Normalized(Value); /// Controls conversion from `Value` to `Expr` #[derive(Copy, Clone)] @@ -81,9 +81,8 @@ impl Resolved { pub fn typecheck(self) -> Result { Ok(typecheck::typecheck(self.0)?.into_typed()) } - pub fn typecheck_with(self, ty: &Typed) -> Result { - Ok(typecheck::typecheck_with(self.0, ty.normalize_to_expr())? - .into_typed()) + pub fn typecheck_with(self, ty: &Normalized) -> Result { + Ok(typecheck::typecheck_with(self.0, ty.to_expr())?.into_typed()) } /// Converts a value back to the corresponding AST expression. pub fn to_expr(&self) -> ResolvedExpr { @@ -92,39 +91,30 @@ impl Resolved { pub fn tck_and_normalize_new_flow(&self) -> Result { let val = crate::semantics::tck::typecheck::typecheck(&self.0)? .normalize_whnf_noenv(); - Ok(Normalized(Typed(val))) + Ok(Normalized(val)) } } impl Typed { /// Reduce an expression to its normal form, performing beta reduction pub fn normalize(mut self) -> Normalized { - self.normalize_mut(); - Normalized(self) + self.0.normalize_mut(); + Normalized(self.0) } - pub(crate) fn from_const(c: Const) -> Self { - Typed(Value::from_const(c)) - } - pub(crate) fn from_kind_and_type(v: ValueKind, t: Typed) -> Self { - Typed(Value::from_kind_and_type(v, t.into_value())) - } pub(crate) fn from_value(th: Value) -> Self { Typed(th) } - pub(crate) fn const_type() -> Self { - Typed::from_const(Const::Type) - } /// Converts a value back to the corresponding AST expression. - pub fn to_expr(&self) -> ResolvedExpr { + pub(crate) fn to_expr(&self) -> ResolvedExpr { self.0.to_expr(ToExprOptions { alpha: false, normalize: false, }) } /// Converts a value back to the corresponding AST expression, beta-normalizing in the process. - pub fn normalize_to_expr(&self) -> NormalizedExpr { + pub(crate) fn normalize_to_expr(&self) -> NormalizedExpr { self.0.to_expr(ToExprOptions { alpha: false, normalize: true, @@ -138,6 +128,34 @@ impl Typed { normalize: true, }) } + pub(crate) fn into_value(self) -> Value { + self.0 + } + + pub(crate) fn get_type(&self) -> Result { + Ok(self.0.get_type()?.into_typed()) + } +} + +impl Normalized { + pub fn encode(&self) -> Result, EncodeError> { + binary::encode(&self.to_expr()) + } + + pub fn to_expr(&self) -> NormalizedExpr { + // TODO: do it directly + self.to_typed().normalize_to_expr() + } + pub(crate) fn to_expr_alpha(&self) -> NormalizedExpr { + // TODO: do it directly + self.to_typed().normalize_to_expr_alpha() + } + pub(crate) fn to_typed(&self) -> Typed { + Typed(self.0.clone()) + } + pub(crate) fn into_typed(self) -> Typed { + Typed(self.0) + } pub(crate) fn to_value(&self) -> Value { self.0.clone() } @@ -145,64 +163,58 @@ impl Typed { self.0 } - pub(crate) fn normalize_mut(&mut self) { - self.0.normalize_mut() + pub(crate) fn from_const(c: Const) -> Self { + Normalized(Value::from_const(c)) } - - pub(crate) fn get_type(&self) -> Result { - Ok(self.0.get_type()?.into_typed()) + 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_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 { - Typed::from_value(Value::from_builtin(b)) + Normalized::from_value(Value::from_builtin(b)) } - pub fn make_optional_type(t: Typed) -> Self { - Typed::from_value( + pub fn make_optional_type(t: Normalized) -> Self { + Normalized::from_value( Value::from_builtin(Builtin::Optional).app(t.to_value()), ) } - pub fn make_list_type(t: Typed) -> Self { - Typed::from_value(Value::from_builtin(Builtin::List).app(t.to_value())) + pub fn make_list_type(t: Normalized) -> Self { + Normalized::from_value( + Value::from_builtin(Builtin::List).app(t.to_value()), + ) } pub fn make_record_type( - kts: impl Iterator, + kts: impl Iterator, ) -> Self { - Typed::from_kind_and_type( + Normalized::from_kind_and_type( ValueKind::RecordType( kts.map(|(k, t)| (k.into(), t.into_value())).collect(), ), - Typed::const_type(), + Normalized::const_type(), ) } pub fn make_union_type( - kts: impl Iterator)>, + kts: impl Iterator)>, ) -> Self { - Typed::from_kind_and_type( + Normalized::from_kind_and_type( ValueKind::UnionType( kts.map(|(k, t)| (k.into(), t.map(|t| t.into_value()))) .collect(), ), - Typed::const_type(), + Normalized::const_type(), ) } } -impl Normalized { - pub fn encode(&self) -> Result, EncodeError> { - binary::encode(&self.to_expr()) - } - - pub(crate) fn to_expr(&self) -> NormalizedExpr { - self.0.normalize_to_expr() - } - pub(crate) fn to_expr_alpha(&self) -> NormalizedExpr { - self.0.normalize_to_expr_alpha() - } - pub(crate) fn into_typed(self) -> Typed { - self.0 - } -} - macro_rules! derive_traits_for_wrapper_struct { ($ty:ident) => { impl std::cmp::PartialEq for $ty { @@ -226,7 +238,6 @@ macro_rules! derive_traits_for_wrapper_struct { derive_traits_for_wrapper_struct!(Parsed); derive_traits_for_wrapper_struct!(Resolved); -derive_traits_for_wrapper_struct!(Normalized); impl std::hash::Hash for Normalized { fn hash(&self, state: &mut H) @@ -245,9 +256,20 @@ impl PartialEq for Typed { self.0 == other.0 } } - impl Display for Typed { 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 { + fn eq(&self, other: &Self) -> bool { + self.0 == other.0 + } +} +impl Display for Normalized { + fn fmt(&self, f: &mut std::fmt::Formatter) -> Result<(), std::fmt::Error> { + self.to_expr().fmt(f) + } +} -- cgit v1.2.3 From 1e466a20533d936f44430b1bc18508cd00e5ccd2 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Wed, 29 Jan 2020 18:48:19 +0000 Subject: Use TyExpr in Typed --- dhall/src/semantics/phase/mod.rs | 69 +++++++++++++++------------------------- 1 file changed, 26 insertions(+), 43 deletions(-) (limited to 'dhall/src/semantics/phase/mod.rs') diff --git a/dhall/src/semantics/phase/mod.rs b/dhall/src/semantics/phase/mod.rs index 68c32b2..0f8194c 100644 --- a/dhall/src/semantics/phase/mod.rs +++ b/dhall/src/semantics/phase/mod.rs @@ -4,6 +4,7 @@ use std::path::Path; use crate::error::{EncodeError, Error, ImportError, TypeError}; use crate::semantics::core::value::Value; use crate::semantics::core::value::ValueKind; +use crate::semantics::tck::tyexpr::TyExpr; use crate::syntax::binary; use crate::syntax::{Builtin, Const, Expr}; use resolve::ImportRoot; @@ -29,7 +30,7 @@ pub struct Resolved(ResolvedExpr); /// A typed expression #[derive(Debug, Clone)] -pub struct Typed(Value); +pub struct Typed(TyExpr); /// A normalized expression. /// @@ -78,11 +79,14 @@ impl Parsed { } impl Resolved { - pub fn typecheck(self) -> Result { - Ok(typecheck::typecheck(self.0)?.into_typed()) + pub fn typecheck(&self) -> Result { + Ok(Typed(crate::semantics::tck::typecheck::typecheck(&self.0)?)) } pub fn typecheck_with(self, ty: &Normalized) -> Result { - Ok(typecheck::typecheck_with(self.0, ty.to_expr())?.into_typed()) + Ok(Typed(crate::semantics::tck::typecheck::typecheck_with( + &self.0, + ty.to_expr(), + )?)) } /// Converts a value back to the corresponding AST expression. pub fn to_expr(&self) -> ResolvedExpr { @@ -97,43 +101,22 @@ impl Resolved { impl Typed { /// Reduce an expression to its normal form, performing beta reduction - pub fn normalize(mut self) -> Normalized { - self.0.normalize_mut(); - Normalized(self.0) - } - - pub(crate) fn from_value(th: Value) -> Self { - Typed(th) + pub fn normalize(&self) -> Normalized { + let mut val = self.0.normalize_whnf_noenv(); + val.normalize_mut(); + Normalized(val) } /// Converts a value back to the corresponding AST expression. - pub(crate) fn to_expr(&self) -> ResolvedExpr { + fn to_expr(&self) -> ResolvedExpr { self.0.to_expr(ToExprOptions { alpha: false, normalize: false, }) } - /// Converts a value back to the corresponding AST expression, beta-normalizing in the process. - pub(crate) fn normalize_to_expr(&self) -> NormalizedExpr { - self.0.to_expr(ToExprOptions { - alpha: false, - normalize: true, - }) - } - /// Converts a value back to the corresponding AST expression, (alpha,beta)-normalizing in the - /// process. - pub(crate) fn normalize_to_expr_alpha(&self) -> NormalizedExpr { - self.0.to_expr(ToExprOptions { - alpha: true, - normalize: true, - }) - } - pub(crate) fn into_value(self) -> Value { - self.0 - } - pub(crate) fn get_type(&self) -> Result { - Ok(self.0.get_type()?.into_typed()) + pub(crate) fn get_type(&self) -> Result { + Ok(Normalized(self.0.get_type()?)) } } @@ -142,19 +125,19 @@ impl Normalized { binary::encode(&self.to_expr()) } + /// Converts a value back to the corresponding AST expression. pub fn to_expr(&self) -> NormalizedExpr { - // TODO: do it directly - self.to_typed().normalize_to_expr() + self.0.to_expr(ToExprOptions { + alpha: false, + normalize: false, + }) } + /// Converts a value back to the corresponding AST expression, alpha-normalizing in the process. pub(crate) fn to_expr_alpha(&self) -> NormalizedExpr { - // TODO: do it directly - self.to_typed().normalize_to_expr_alpha() - } - pub(crate) fn to_typed(&self) -> Typed { - Typed(self.0.clone()) - } - pub(crate) fn into_typed(self) -> Typed { - Typed(self.0) + self.0.to_expr(ToExprOptions { + alpha: true, + normalize: false, + }) } pub(crate) fn to_value(&self) -> Value { self.0.clone() @@ -253,7 +236,7 @@ impl std::hash::Hash for Normalized { impl Eq for Typed {} impl PartialEq for Typed { fn eq(&self, other: &Self) -> bool { - self.0 == other.0 + self.normalize() == other.normalize() } } impl Display for Typed { -- cgit v1.2.3 From e410dbb428e621fe600be43ddecca1c7bff7cb2f Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Wed, 29 Jan 2020 19:11:52 +0000 Subject: Fix insufficient normalization --- dhall/src/semantics/phase/mod.rs | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) (limited to 'dhall/src/semantics/phase/mod.rs') diff --git a/dhall/src/semantics/phase/mod.rs b/dhall/src/semantics/phase/mod.rs index 0f8194c..2727a61 100644 --- a/dhall/src/semantics/phase/mod.rs +++ b/dhall/src/semantics/phase/mod.rs @@ -102,9 +102,7 @@ impl Resolved { impl Typed { /// Reduce an expression to its normal form, performing beta reduction pub fn normalize(&self) -> Normalized { - let mut val = self.0.normalize_whnf_noenv(); - val.normalize_mut(); - Normalized(val) + Normalized(self.0.normalize_nf_noenv()) } /// Converts a value back to the corresponding AST expression. -- cgit v1.2.3 From 7743647137d1914c280e03d6aaee81e507cff97d Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Thu, 30 Jan 2020 11:17:49 +0000 Subject: Remove old typecheck module --- dhall/src/semantics/phase/mod.rs | 17 +++-------------- 1 file changed, 3 insertions(+), 14 deletions(-) (limited to 'dhall/src/semantics/phase/mod.rs') diff --git a/dhall/src/semantics/phase/mod.rs b/dhall/src/semantics/phase/mod.rs index 2727a61..f24a668 100644 --- a/dhall/src/semantics/phase/mod.rs +++ b/dhall/src/semantics/phase/mod.rs @@ -2,9 +2,7 @@ use std::fmt::Display; use std::path::Path; use crate::error::{EncodeError, Error, ImportError, TypeError}; -use crate::semantics::core::value::Value; -use crate::semantics::core::value::ValueKind; -use crate::semantics::tck::tyexpr::TyExpr; +use crate::semantics::{typecheck, typecheck_with, TyExpr, Value, ValueKind}; use crate::syntax::binary; use crate::syntax::{Builtin, Const, Expr}; use resolve::ImportRoot; @@ -12,7 +10,6 @@ use resolve::ImportRoot; pub(crate) mod normalize; pub(crate) mod parse; pub(crate) mod resolve; -pub(crate) mod typecheck; pub type ParsedExpr = Expr; pub type DecodedExpr = Expr; @@ -80,23 +77,15 @@ impl Parsed { impl Resolved { pub fn typecheck(&self) -> Result { - Ok(Typed(crate::semantics::tck::typecheck::typecheck(&self.0)?)) + Ok(Typed(typecheck(&self.0)?)) } pub fn typecheck_with(self, ty: &Normalized) -> Result { - Ok(Typed(crate::semantics::tck::typecheck::typecheck_with( - &self.0, - ty.to_expr(), - )?)) + Ok(Typed(typecheck_with(&self.0, ty.to_expr())?)) } /// Converts a value back to the corresponding AST expression. pub fn to_expr(&self) -> ResolvedExpr { self.0.clone() } - pub fn tck_and_normalize_new_flow(&self) -> Result { - let val = crate::semantics::tck::typecheck::typecheck(&self.0)? - .normalize_whnf_noenv(); - Ok(Normalized(val)) - } } impl Typed { -- cgit v1.2.3 From 67bbbafbc9730d74e20e5ac082ae9a87bdf2234e Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Thu, 30 Jan 2020 16:39:25 +0000 Subject: Introduce Thunks and normalize lazily --- dhall/src/semantics/phase/mod.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'dhall/src/semantics/phase/mod.rs') diff --git a/dhall/src/semantics/phase/mod.rs b/dhall/src/semantics/phase/mod.rs index f24a668..a25f096 100644 --- a/dhall/src/semantics/phase/mod.rs +++ b/dhall/src/semantics/phase/mod.rs @@ -91,7 +91,7 @@ impl Resolved { impl Typed { /// Reduce an expression to its normal form, performing beta reduction pub fn normalize(&self) -> Normalized { - Normalized(self.0.normalize_nf_noenv()) + Normalized(self.0.rec_eval_closed_expr()) } /// Converts a value back to the corresponding AST expression. -- cgit v1.2.3 From 653cdb44cec4f54697d18f2c4ae9f67bbbc2fb3d Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Thu, 30 Jan 2020 17:04:28 +0000 Subject: Move normalize under nze --- dhall/src/semantics/phase/mod.rs | 1 - 1 file changed, 1 deletion(-) (limited to 'dhall/src/semantics/phase/mod.rs') diff --git a/dhall/src/semantics/phase/mod.rs b/dhall/src/semantics/phase/mod.rs index a25f096..ff4b859 100644 --- a/dhall/src/semantics/phase/mod.rs +++ b/dhall/src/semantics/phase/mod.rs @@ -7,7 +7,6 @@ use crate::syntax::binary; use crate::syntax::{Builtin, Const, Expr}; use resolve::ImportRoot; -pub(crate) mod normalize; pub(crate) mod parse; pub(crate) mod resolve; -- cgit v1.2.3 From 5197c26c23edd6c499f8e0f8a239fe4393b2e3d2 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Thu, 30 Jan 2020 17:09:16 +0000 Subject: Move main API to lib.rs --- dhall/src/semantics/phase/mod.rs | 242 --------------------------------------- 1 file changed, 242 deletions(-) (limited to 'dhall/src/semantics/phase/mod.rs') diff --git a/dhall/src/semantics/phase/mod.rs b/dhall/src/semantics/phase/mod.rs index ff4b859..02e2b18 100644 --- a/dhall/src/semantics/phase/mod.rs +++ b/dhall/src/semantics/phase/mod.rs @@ -1,244 +1,2 @@ -use std::fmt::Display; -use std::path::Path; - -use crate::error::{EncodeError, Error, ImportError, TypeError}; -use crate::semantics::{typecheck, typecheck_with, TyExpr, Value, ValueKind}; -use crate::syntax::binary; -use crate::syntax::{Builtin, Const, Expr}; -use resolve::ImportRoot; - pub(crate) mod parse; pub(crate) mod resolve; - -pub type ParsedExpr = Expr; -pub type DecodedExpr = Expr; -pub type ResolvedExpr = Expr; -pub type NormalizedExpr = Expr; - -#[derive(Debug, Clone)] -pub struct Parsed(ParsedExpr, ImportRoot); - -/// An expression where all imports have been resolved -/// -/// Invariant: there must be no `Import` nodes or `ImportAlt` operations left. -#[derive(Debug, Clone)] -pub struct Resolved(ResolvedExpr); - -/// A typed expression -#[derive(Debug, Clone)] -pub struct Typed(TyExpr); - -/// A normalized expression. -/// -/// Invariant: the contained Typed expression must be in normal form, -#[derive(Debug, Clone)] -pub struct Normalized(Value); - -/// Controls conversion from `Value` to `Expr` -#[derive(Copy, Clone)] -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 { - pub fn parse_file(f: &Path) -> Result { - parse::parse_file(f) - } - pub fn parse_str(s: &str) -> Result { - parse::parse_str(s) - } - pub fn parse_binary_file(f: &Path) -> Result { - parse::parse_binary_file(f) - } - pub fn parse_binary(data: &[u8]) -> Result { - parse::parse_binary(data) - } - - pub fn resolve(self) -> Result { - resolve::resolve(self) - } - pub fn skip_resolve(self) -> Result { - resolve::skip_resolve_expr(self) - } - - pub fn encode(&self) -> Result, EncodeError> { - binary::encode(&self.0) - } - - /// Converts a value back to the corresponding AST expression. - pub fn to_expr(&self) -> ParsedExpr { - self.0.clone() - } -} - -impl Resolved { - pub fn typecheck(&self) -> Result { - Ok(Typed(typecheck(&self.0)?)) - } - pub fn typecheck_with(self, ty: &Normalized) -> Result { - Ok(Typed(typecheck_with(&self.0, ty.to_expr())?)) - } - /// Converts a value back to the corresponding AST expression. - pub fn to_expr(&self) -> ResolvedExpr { - self.0.clone() - } -} - -impl Typed { - /// Reduce an expression to its normal form, performing beta reduction - pub fn normalize(&self) -> Normalized { - Normalized(self.0.rec_eval_closed_expr()) - } - - /// Converts a value back to the corresponding AST expression. - fn to_expr(&self) -> ResolvedExpr { - self.0.to_expr(ToExprOptions { - alpha: false, - normalize: false, - }) - } - - pub(crate) fn get_type(&self) -> Result { - Ok(Normalized(self.0.get_type()?)) - } -} - -impl Normalized { - pub fn encode(&self) -> Result, EncodeError> { - binary::encode(&self.to_expr()) - } - - /// Converts a value back to the corresponding AST expression. - pub fn to_expr(&self) -> NormalizedExpr { - self.0.to_expr(ToExprOptions { - alpha: false, - normalize: false, - }) - } - /// 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, - }) - } - pub(crate) fn to_value(&self) -> Value { - self.0.clone() - } - pub(crate) fn into_value(self) -> Value { - 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_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)) - } - pub fn make_optional_type(t: Normalized) -> Self { - Normalized::from_value( - Value::from_builtin(Builtin::Optional).app(t.to_value()), - ) - } - pub fn make_list_type(t: Normalized) -> Self { - Normalized::from_value( - Value::from_builtin(Builtin::List).app(t.to_value()), - ) - } - 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(), - ) - } - 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(), - ) - } -} - -macro_rules! derive_traits_for_wrapper_struct { - ($ty:ident) => { - impl std::cmp::PartialEq for $ty { - fn eq(&self, other: &Self) -> bool { - self.0 == other.0 - } - } - - impl std::cmp::Eq for $ty {} - - impl std::fmt::Display for $ty { - fn fmt( - &self, - f: &mut std::fmt::Formatter, - ) -> Result<(), std::fmt::Error> { - self.0.fmt(f) - } - } - }; -} - -derive_traits_for_wrapper_struct!(Parsed); -derive_traits_for_wrapper_struct!(Resolved); - -impl std::hash::Hash for Normalized { - fn hash(&self, state: &mut H) - where - H: std::hash::Hasher, - { - if let Ok(vec) = self.encode() { - vec.hash(state) - } - } -} - -impl Eq for Typed {} -impl PartialEq for Typed { - fn eq(&self, other: &Self) -> bool { - self.normalize() == other.normalize() - } -} -impl Display for Typed { - 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 { - fn eq(&self, other: &Self) -> bool { - self.0 == other.0 - } -} -impl Display for Normalized { - fn fmt(&self, f: &mut std::fmt::Formatter) -> Result<(), std::fmt::Error> { - self.to_expr().fmt(f) - } -} -- cgit v1.2.3 From 8ff022fa2cec34bc1d46ac3655d0c3d228ef893c Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Thu, 30 Jan 2020 17:16:25 +0000 Subject: Move parse and resolve up a level --- dhall/src/semantics/phase/mod.rs | 2 -- 1 file changed, 2 deletions(-) delete mode 100644 dhall/src/semantics/phase/mod.rs (limited to 'dhall/src/semantics/phase/mod.rs') diff --git a/dhall/src/semantics/phase/mod.rs b/dhall/src/semantics/phase/mod.rs deleted file mode 100644 index 02e2b18..0000000 --- a/dhall/src/semantics/phase/mod.rs +++ /dev/null @@ -1,2 +0,0 @@ -pub(crate) mod parse; -pub(crate) mod resolve; -- cgit v1.2.3