From 7abd49772643ee4e131ef47de66db22ba7c1e037 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Sun, 15 Dec 2019 19:47:20 +0000 Subject: Move contents of dhall under a semantics submodule --- dhall/src/semantics/phase/mod.rs | 254 +++++++++++++++++++++++++++++++++++++++ 1 file changed, 254 insertions(+) create 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 new file mode 100644 index 0000000..918c4d0 --- /dev/null +++ b/dhall/src/semantics/phase/mod.rs @@ -0,0 +1,254 @@ +use std::fmt::Display; +use std::path::Path; + +use crate::syntax::{Builtin, Const, Expr}; + +use crate::core::value::{ToExprOptions, Value}; +use crate::core::valuef::ValueF; +use crate::core::var::{AlphaVar, Shift, Subst}; +use crate::error::{EncodeError, Error, ImportError, TypeError}; + +use resolve::ImportRoot; + +pub(crate) mod binary; +pub(crate) mod normalize; +pub(crate) mod parse; +pub(crate) mod resolve; +pub(crate) mod typecheck; + +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(Value); + +/// A normalized expression. +/// +/// Invariant: the contained Typed expression must be in normal form, +#[derive(Debug, Clone)] +pub struct Normalized(Typed); + +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> { + crate::phase::binary::encode(&self.0) + } +} + +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()) + } +} + +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) + } + + 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_value(th: Value) -> Self { + Typed(th) + } + pub(crate) fn const_type() -> Self { + Typed::from_const(Const::Type) + } + + pub(crate) fn to_expr(&self) -> NormalizedExpr { + self.0.to_expr(ToExprOptions { + alpha: false, + normalize: false, + }) + } + pub fn normalize_to_expr(&self) -> NormalizedExpr { + self.0.to_expr(ToExprOptions { + alpha: false, + normalize: true, + }) + } + pub(crate) fn normalize_to_expr_alpha(&self) -> NormalizedExpr { + self.0.to_expr(ToExprOptions { + alpha: true, + normalize: true, + }) + } + pub(crate) fn to_value(&self) -> Value { + self.0.clone() + } + pub(crate) fn into_value(self) -> Value { + self.0 + } + + pub(crate) fn normalize_mut(&mut self) { + self.0.normalize_mut() + } + + pub(crate) fn get_type(&self) -> Result { + Ok(self.0.get_type()?.into_typed()) + } + + pub fn make_builtin_type(b: Builtin) -> Self { + Typed::from_value(Value::from_builtin(b)) + } + pub fn make_optional_type(t: Typed) -> Self { + Typed::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_record_type( + kts: impl Iterator, + ) -> Self { + Typed::from_valuef_and_type( + ValueF::RecordType( + kts.map(|(k, t)| (k.into(), t.into_value())).collect(), + ), + Typed::const_type(), + ) + } + pub fn make_union_type( + kts: impl Iterator)>, + ) -> Self { + Typed::from_valuef_and_type( + ValueF::UnionType( + kts.map(|(k, t)| (k.into(), t.map(|t| t.into_value()))) + .collect(), + ), + Typed::const_type(), + ) + } +} + +impl Normalized { + pub fn encode(&self) -> Result, EncodeError> { + crate::phase::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 + } +} + +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)?)) + } +} + +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 { + 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); +derive_traits_for_wrapper_struct!(Normalized); + +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.0 == other.0 + } +} + +impl Display for Typed { + fn fmt(&self, f: &mut std::fmt::Formatter) -> Result<(), std::fmt::Error> { + self.to_expr().fmt(f) + } +} -- cgit v1.2.3 From 0105e3c31dbb2984e5c4b9d51cc3b27767e7683c Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Sun, 15 Dec 2019 19:56:54 +0000 Subject: Avoid mention of `crate::` outside of top-level imports --- dhall/src/semantics/phase/mod.rs | 8 +++----- 1 file changed, 3 insertions(+), 5 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 918c4d0..9f38308 100644 --- a/dhall/src/semantics/phase/mod.rs +++ b/dhall/src/semantics/phase/mod.rs @@ -1,13 +1,11 @@ use std::fmt::Display; use std::path::Path; -use crate::syntax::{Builtin, Const, Expr}; - use crate::core::value::{ToExprOptions, Value}; use crate::core::valuef::ValueF; use crate::core::var::{AlphaVar, Shift, Subst}; use crate::error::{EncodeError, Error, ImportError, TypeError}; - +use crate::syntax::{Builtin, Const, Expr}; use resolve::ImportRoot; pub(crate) mod binary; @@ -62,7 +60,7 @@ impl Parsed { } pub fn encode(&self) -> Result, EncodeError> { - crate::phase::binary::encode(&self.0) + binary::encode(&self.0) } } @@ -172,7 +170,7 @@ impl Typed { impl Normalized { pub fn encode(&self) -> Result, EncodeError> { - crate::phase::binary::encode(&self.to_expr()) + binary::encode(&self.to_expr()) } pub(crate) fn to_expr(&self) -> NormalizedExpr { -- cgit v1.2.3 From b11a2cd6ca50d5a4dfa71ae8cd0642fb1c75e1cf Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Sun, 15 Dec 2019 20:01:35 +0000 Subject: Refer to semantics module properly --- dhall/src/semantics/phase/mod.rs | 8 ++++---- 1 file changed, 4 insertions(+), 4 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 9f38308..0d8fc75 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::core::value::{ToExprOptions, Value}; -use crate::core::valuef::ValueF; -use crate::core::var::{AlphaVar, Shift, Subst}; -use crate::error::{EncodeError, Error, ImportError, TypeError}; +use crate::semantics::core::value::{ToExprOptions, Value}; +use crate::semantics::core::valuef::ValueF; +use crate::semantics::core::var::{AlphaVar, Shift, Subst}; +use crate::semantics::error::{EncodeError, Error, ImportError, TypeError}; use crate::syntax::{Builtin, Const, Expr}; use resolve::ImportRoot; -- cgit v1.2.3 From 97d5840ef607e9eedb1801c7711684908af82b60 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Tue, 17 Dec 2019 11:51:57 +0000 Subject: Move binary encoding/decoding to syntax/ --- 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 0d8fc75..752c257 100644 --- a/dhall/src/semantics/phase/mod.rs +++ b/dhall/src/semantics/phase/mod.rs @@ -5,10 +5,10 @@ use crate::semantics::core::value::{ToExprOptions, Value}; use crate::semantics::core::valuef::ValueF; use crate::semantics::core::var::{AlphaVar, Shift, Subst}; use crate::semantics::error::{EncodeError, Error, ImportError, TypeError}; +use crate::syntax::binary; use crate::syntax::{Builtin, Const, Expr}; use resolve::ImportRoot; -pub(crate) mod binary; pub(crate) mod normalize; pub(crate) mod parse; pub(crate) mod resolve; -- cgit v1.2.3