From 30bbf22fbfaead80322888eba7b7acdf908c3f3e Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Tue, 17 Dec 2019 15:00:44 +0000 Subject: Rename ValueF to ValueKind --- dhall/src/semantics/phase/mod.rs | 14 +++++++------- 1 file changed, 7 insertions(+), 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 752c257..f27088c 100644 --- a/dhall/src/semantics/phase/mod.rs +++ b/dhall/src/semantics/phase/mod.rs @@ -2,7 +2,7 @@ use std::fmt::Display; use std::path::Path; use crate::semantics::core::value::{ToExprOptions, Value}; -use crate::semantics::core::valuef::ValueF; +use crate::semantics::core::value_kind::ValueKind; use crate::semantics::core::var::{AlphaVar, Shift, Subst}; use crate::semantics::error::{EncodeError, Error, ImportError, TypeError}; use crate::syntax::binary; @@ -91,8 +91,8 @@ impl Typed { pub(crate) fn from_const(c: Const) -> Self { Typed(Value::from_const(c)) } - pub(crate) fn from_valuef_and_type(v: ValueF, t: Typed) -> Self { - Typed(Value::from_valuef_and_type(v, t.into_value())) + 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) @@ -148,8 +148,8 @@ impl Typed { pub fn make_record_type( kts: impl Iterator, ) -> Self { - Typed::from_valuef_and_type( - ValueF::RecordType( + Typed::from_kind_and_type( + ValueKind::RecordType( kts.map(|(k, t)| (k.into(), t.into_value())).collect(), ), Typed::const_type(), @@ -158,8 +158,8 @@ impl Typed { pub fn make_union_type( kts: impl Iterator)>, ) -> Self { - Typed::from_valuef_and_type( - ValueF::UnionType( + Typed::from_kind_and_type( + ValueKind::UnionType( kts.map(|(k, t)| (k.into(), t.map(|t| t.into_value()))) .collect(), ), -- cgit v1.2.3 From fd665388b6f1fd80ded9010640ac65cfebca7bc6 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Tue, 17 Dec 2019 16:00:51 +0000 Subject: Move out conversion from value back to ast to its own file --- dhall/src/semantics/phase/mod.rs | 7 ++++++- 1 file changed, 6 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 f27088c..6229d15 100644 --- a/dhall/src/semantics/phase/mod.rs +++ b/dhall/src/semantics/phase/mod.rs @@ -1,10 +1,11 @@ use std::fmt::Display; use std::path::Path; -use crate::semantics::core::value::{ToExprOptions, Value}; +use crate::semantics::core::value::Value; use crate::semantics::core::value_kind::ValueKind; use crate::semantics::core::var::{AlphaVar, Shift, Subst}; use crate::semantics::error::{EncodeError, Error, ImportError, TypeError}; +use crate::semantics::to_expr::ToExprOptions; use crate::syntax::binary; use crate::syntax::{Builtin, Const, Expr}; use resolve::ImportRoot; @@ -101,18 +102,22 @@ impl Typed { Typed::from_const(Const::Type) } + /// Converts a value back to the corresponding AST expression. pub(crate) fn to_expr(&self) -> NormalizedExpr { self.0.to_expr(ToExprOptions { alpha: false, normalize: false, }) } + /// Converts a value back to the corresponding AST expression, normalizing in the process. pub fn normalize_to_expr(&self) -> NormalizedExpr { self.0.to_expr(ToExprOptions { alpha: false, normalize: true, }) } + /// Converts a value back to the corresponding AST expression, (akpha,beta)-normalizing in the + /// process. pub(crate) fn normalize_to_expr_alpha(&self) -> NormalizedExpr { self.0.to_expr(ToExprOptions { alpha: true, -- cgit v1.2.3 From 78d066a44c5598794602effa4c10a09f80ed1e72 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Fri, 20 Dec 2019 17:57:49 +0000 Subject: Move error module to root of crate --- 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 6229d15..9359c0b 100644 --- a/dhall/src/semantics/phase/mod.rs +++ b/dhall/src/semantics/phase/mod.rs @@ -1,10 +1,10 @@ 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_kind::ValueKind; use crate::semantics::core::var::{AlphaVar, Shift, Subst}; -use crate::semantics::error::{EncodeError, Error, ImportError, TypeError}; use crate::semantics::to_expr::ToExprOptions; use crate::syntax::binary; use crate::syntax::{Builtin, Const, Expr}; -- cgit v1.2.3 From 5c15f643236c5e14c2e8797b9dc507cffc93c43a Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Fri, 20 Dec 2019 19:15:10 +0000 Subject: Fix some comments --- dhall/src/semantics/phase/mod.rs | 11 ++--------- 1 file changed, 2 insertions(+), 9 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 9359c0b..7c57c3f 100644 --- a/dhall/src/semantics/phase/mod.rs +++ b/dhall/src/semantics/phase/mod.rs @@ -77,13 +77,6 @@ impl Resolved { impl Typed { /// Reduce an expression to its normal form, performing beta reduction - /// - /// `normalize` does not type-check the expression. You may want to type-check - /// expressions before normalizing them since normalization can convert an - /// ill-typed expression into a well-typed expression. - /// - /// However, `normalize` will not fail if the expression is ill-typed and will - /// leave ill-typed sub-expressions unevaluated. pub fn normalize(mut self) -> Normalized { self.normalize_mut(); Normalized(self) @@ -109,14 +102,14 @@ impl Typed { normalize: false, }) } - /// Converts a value back to the corresponding AST expression, normalizing in the process. + /// Converts a value back to the corresponding AST expression, beta-normalizing in the process. pub fn normalize_to_expr(&self) -> NormalizedExpr { self.0.to_expr(ToExprOptions { alpha: false, normalize: true, }) } - /// Converts a value back to the corresponding AST expression, (akpha,beta)-normalizing in the + /// 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 { -- cgit v1.2.3 From 64cca1837cc97b7679c4e2ffd54a22ad50f05cfd Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Fri, 20 Dec 2019 19:26:08 +0000 Subject: Move ValueKind into value.rs --- 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 7c57c3f..b22120d 100644 --- a/dhall/src/semantics/phase/mod.rs +++ b/dhall/src/semantics/phase/mod.rs @@ -3,7 +3,7 @@ use std::path::Path; use crate::error::{EncodeError, Error, ImportError, TypeError}; use crate::semantics::core::value::Value; -use crate::semantics::core::value_kind::ValueKind; +use crate::semantics::core::value::ValueKind; use crate::semantics::core::var::{AlphaVar, Shift, Subst}; use crate::semantics::to_expr::ToExprOptions; use crate::syntax::binary; -- cgit v1.2.3