diff options
author | Nadrieril | 2020-01-30 17:09:16 +0000 |
---|---|---|
committer | Nadrieril | 2020-01-30 17:09:16 +0000 |
commit | 5197c26c23edd6c499f8e0f8a239fe4393b2e3d2 (patch) | |
tree | 49c8678bf2e696720cc1dcc91d4f80bdbe031203 /dhall/src/semantics | |
parent | 653cdb44cec4f54697d18f2c4ae9f67bbbc2fb3d (diff) |
Move main API to lib.rs
Diffstat (limited to '')
-rw-r--r-- | dhall/src/semantics/builtins.rs | 2 | ||||
-rw-r--r-- | dhall/src/semantics/nze/normalize.rs | 2 | ||||
-rw-r--r-- | dhall/src/semantics/nze/value.rs | 2 | ||||
-rw-r--r-- | dhall/src/semantics/phase/mod.rs | 242 | ||||
-rw-r--r-- | dhall/src/semantics/phase/parse.rs | 2 | ||||
-rw-r--r-- | dhall/src/semantics/phase/resolve.rs | 2 | ||||
-rw-r--r-- | dhall/src/semantics/tck/tyexpr.rs | 4 | ||||
-rw-r--r-- | dhall/src/semantics/tck/typecheck.rs | 2 |
8 files changed, 8 insertions, 250 deletions
diff --git a/dhall/src/semantics/builtins.rs b/dhall/src/semantics/builtins.rs index 9d10d89..2211579 100644 --- a/dhall/src/semantics/builtins.rs +++ b/dhall/src/semantics/builtins.rs @@ -1,4 +1,3 @@ -use crate::semantics::phase::Normalized; use crate::semantics::{ typecheck, NzEnv, TyExpr, TyExprKind, Value, ValueKind, VarEnv, }; @@ -8,6 +7,7 @@ use crate::syntax::{ BinOp, Builtin, Const, Expr, ExprKind, InterpolatedText, InterpolatedTextContents, Label, NaiveDouble, Span, UnspannedExpr, V, }; +use crate::Normalized; use std::collections::HashMap; use std::convert::TryInto; diff --git a/dhall/src/semantics/nze/normalize.rs b/dhall/src/semantics/nze/normalize.rs index ea1a25b..6564018 100644 --- a/dhall/src/semantics/nze/normalize.rs +++ b/dhall/src/semantics/nze/normalize.rs @@ -1,6 +1,5 @@ use std::collections::HashMap; -use crate::semantics::phase::Normalized; use crate::semantics::NzEnv; use crate::semantics::{ Binder, BuiltinClosure, Closure, TyExpr, TyExprKind, Value, ValueKind, @@ -8,6 +7,7 @@ use crate::semantics::{ use crate::syntax::{ BinOp, Builtin, Const, ExprKind, InterpolatedTextContents, }; +use crate::Normalized; pub(crate) fn apply_any(f: Value, a: Value, ty: &Value) -> ValueKind<Value> { let f_borrow = f.kind(); diff --git a/dhall/src/semantics/nze/value.rs b/dhall/src/semantics/nze/value.rs index 215c342..0a9de6a 100644 --- a/dhall/src/semantics/nze/value.rs +++ b/dhall/src/semantics/nze/value.rs @@ -4,7 +4,6 @@ use std::rc::Rc; use crate::error::{TypeError, TypeMessage}; use crate::semantics::nze::visitor; -use crate::semantics::phase::{Normalized, NormalizedExpr, ToExprOptions}; use crate::semantics::Binder; use crate::semantics::{apply_any, normalize_tyexpr_whnf, normalize_whnf}; use crate::semantics::{type_of_builtin, typecheck, TyExpr, TyExprKind}; @@ -13,6 +12,7 @@ use crate::syntax::{ BinOp, Builtin, Const, ExprKind, Integer, InterpolatedTextContents, Label, NaiveDouble, Natural, Span, }; +use crate::{Normalized, NormalizedExpr, ToExprOptions}; use self::Form::{Unevaled, WHNF}; 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<Normalized>; -pub type DecodedExpr = Expr<Normalized>; -pub type ResolvedExpr = Expr<Normalized>; -pub type NormalizedExpr = Expr<Normalized>; - -#[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<Parsed, Error> { - parse::parse_file(f) - } - pub fn parse_str(s: &str) -> Result<Parsed, Error> { - parse::parse_str(s) - } - pub fn parse_binary_file(f: &Path) -> Result<Parsed, Error> { - parse::parse_binary_file(f) - } - pub fn parse_binary(data: &[u8]) -> Result<Parsed, Error> { - parse::parse_binary(data) - } - - pub fn resolve(self) -> Result<Resolved, ImportError> { - resolve::resolve(self) - } - pub fn skip_resolve(self) -> Result<Resolved, ImportError> { - resolve::skip_resolve_expr(self) - } - - pub fn encode(&self) -> Result<Vec<u8>, 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<Typed, TypeError> { - Ok(Typed(typecheck(&self.0)?)) - } - pub fn typecheck_with(self, ty: &Normalized) -> Result<Typed, TypeError> { - 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<Normalized, TypeError> { - Ok(Normalized(self.0.get_type()?)) - } -} - -impl Normalized { - pub fn encode(&self) -> Result<Vec<u8>, 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<Value>, - 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<Item = (String, Normalized)>, - ) -> 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<Item = (String, Option<Normalized>)>, - ) -> 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<H>(&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) - } -} diff --git a/dhall/src/semantics/phase/parse.rs b/dhall/src/semantics/phase/parse.rs index 00db422..b72fe7f 100644 --- a/dhall/src/semantics/phase/parse.rs +++ b/dhall/src/semantics/phase/parse.rs @@ -4,9 +4,9 @@ use std::path::Path; use crate::error::Error; use crate::semantics::phase::resolve::ImportRoot; -use crate::semantics::phase::Parsed; use crate::syntax::binary; use crate::syntax::parse_expr; +use crate::Parsed; pub(crate) fn parse_file(f: &Path) -> Result<Parsed, Error> { let mut buffer = String::new(); diff --git a/dhall/src/semantics/phase/resolve.rs b/dhall/src/semantics/phase/resolve.rs index cc4a024..3acf114 100644 --- a/dhall/src/semantics/phase/resolve.rs +++ b/dhall/src/semantics/phase/resolve.rs @@ -2,9 +2,9 @@ use std::collections::HashMap; use std::path::{Path, PathBuf}; use crate::error::{Error, ImportError}; -use crate::semantics::phase::{Normalized, NormalizedExpr, Parsed, Resolved}; use crate::syntax; use crate::syntax::{FilePath, ImportLocation, URL}; +use crate::{Normalized, NormalizedExpr, Parsed, Resolved}; type Import = syntax::Import<NormalizedExpr>; diff --git a/dhall/src/semantics/tck/tyexpr.rs b/dhall/src/semantics/tck/tyexpr.rs index 98dc3f9..4b88048 100644 --- a/dhall/src/semantics/tck/tyexpr.rs +++ b/dhall/src/semantics/tck/tyexpr.rs @@ -1,9 +1,9 @@ use crate::error::{TypeError, TypeMessage}; use crate::semantics::normalize_tyexpr_whnf; -use crate::semantics::phase::Normalized; -use crate::semantics::phase::{NormalizedExpr, ToExprOptions}; use crate::semantics::{rc, NameEnv, NzEnv, TyEnv, Value}; use crate::syntax::{ExprKind, Span, V}; +use crate::Normalized; +use crate::{NormalizedExpr, ToExprOptions}; pub(crate) type Type = Value; diff --git a/dhall/src/semantics/tck/typecheck.rs b/dhall/src/semantics/tck/typecheck.rs index 348471f..212e6e7 100644 --- a/dhall/src/semantics/tck/typecheck.rs +++ b/dhall/src/semantics/tck/typecheck.rs @@ -4,7 +4,6 @@ use std::collections::HashMap; use crate::error::{TypeError, TypeMessage}; use crate::semantics::merge_maps; -use crate::semantics::phase::Normalized; use crate::semantics::{ type_of_builtin, Binder, BuiltinClosure, Closure, TyEnv, TyExpr, TyExprKind, Type, Value, ValueKind, @@ -12,6 +11,7 @@ use crate::semantics::{ use crate::syntax::{ BinOp, Builtin, Const, Expr, ExprKind, InterpolatedTextContents, Span, }; +use crate::Normalized; fn type_of_recordtype<'a>( tys: impl Iterator<Item = Cow<'a, TyExpr>>, |