diff options
author | Nadrieril Feneanar | 2019-12-19 21:33:26 +0000 |
---|---|---|
committer | GitHub | 2019-12-19 21:33:26 +0000 |
commit | 91ef0cf697d56c91a8d15937aa4669dc221cd6c1 (patch) | |
tree | d3f00cf31d4386b82c6fb09eda3f690415dd8902 /dhall/src/semantics | |
parent | 3f00e4ca3fe22f88a1d0633e254df0bff781c6d3 (diff) | |
parent | 1e4f15d1891b497ecf6632432bc9252dc6a4507d (diff) |
Merge pull request #117 from Nadrieril/merge-crates
Merge a bunch of sub-crates
Diffstat (limited to '')
-rw-r--r-- | dhall/src/semantics/core/context.rs (renamed from dhall/src/core/context.rs) | 11 | ||||
-rw-r--r-- | dhall/src/semantics/core/mod.rs (renamed from dhall/src/core/mod.rs) | 0 | ||||
-rw-r--r-- | dhall/src/semantics/core/value.rs (renamed from dhall/src/core/value.rs) | 17 | ||||
-rw-r--r-- | dhall/src/semantics/core/valuef.rs (renamed from dhall/src/core/valuef.rs) | 14 | ||||
-rw-r--r-- | dhall/src/semantics/core/var.rs (renamed from dhall/src/core/var.rs) | 10 | ||||
-rw-r--r-- | dhall/src/semantics/error/mod.rs (renamed from dhall/src/error/mod.rs) | 11 | ||||
-rw-r--r-- | dhall/src/semantics/mod.rs | 3 | ||||
-rw-r--r-- | dhall/src/semantics/phase/mod.rs (renamed from dhall/src/phase/mod.rs) | 18 | ||||
-rw-r--r-- | dhall/src/semantics/phase/normalize.rs (renamed from dhall/src/phase/normalize.rs) | 22 | ||||
-rw-r--r-- | dhall/src/semantics/phase/parse.rs (renamed from dhall/src/phase/parse.rs) | 14 | ||||
-rw-r--r-- | dhall/src/semantics/phase/resolve.rs (renamed from dhall/src/phase/resolve.rs) | 13 | ||||
-rw-r--r-- | dhall/src/semantics/phase/typecheck.rs (renamed from dhall/src/phase/typecheck.rs) | 53 |
12 files changed, 90 insertions, 96 deletions
diff --git a/dhall/src/core/context.rs b/dhall/src/semantics/core/context.rs index 2bf39c5..d150e56 100644 --- a/dhall/src/core/context.rs +++ b/dhall/src/semantics/core/context.rs @@ -1,12 +1,11 @@ use std::collections::HashMap; use std::rc::Rc; -use dhall_syntax::{Label, V}; - -use crate::core::value::Value; -use crate::core::valuef::ValueF; -use crate::core::var::{AlphaVar, Shift, Subst}; -use crate::error::TypeError; +use crate::semantics::core::value::Value; +use crate::semantics::core::valuef::ValueF; +use crate::semantics::core::var::{AlphaVar, Shift, Subst}; +use crate::semantics::error::TypeError; +use crate::syntax::{Label, V}; #[derive(Debug, Clone)] enum CtxItem { diff --git a/dhall/src/core/mod.rs b/dhall/src/semantics/core/mod.rs index 08213f7..08213f7 100644 --- a/dhall/src/core/mod.rs +++ b/dhall/src/semantics/core/mod.rs diff --git a/dhall/src/core/value.rs b/dhall/src/semantics/core/value.rs index d4f5131..6e6739f 100644 --- a/dhall/src/core/value.rs +++ b/dhall/src/semantics/core/value.rs @@ -1,15 +1,14 @@ use std::cell::{Ref, RefCell, RefMut}; use std::rc::Rc; -use dhall_syntax::{Builtin, Const, Span}; - -use crate::core::context::TypecheckContext; -use crate::core::valuef::ValueF; -use crate::core::var::{AlphaVar, Shift, Subst}; -use crate::error::{TypeError, TypeMessage}; -use crate::phase::normalize::{apply_any, normalize_whnf}; -use crate::phase::typecheck::{builtin_to_value, const_to_value}; -use crate::phase::{NormalizedExpr, Typed}; +use crate::semantics::core::context::TypecheckContext; +use crate::semantics::core::valuef::ValueF; +use crate::semantics::core::var::{AlphaVar, Shift, Subst}; +use crate::semantics::error::{TypeError, TypeMessage}; +use crate::semantics::phase::normalize::{apply_any, normalize_whnf}; +use crate::semantics::phase::typecheck::{builtin_to_value, const_to_value}; +use crate::semantics::phase::{NormalizedExpr, Typed}; +use crate::syntax::{Builtin, Const, Span}; #[derive(Debug, Clone, Copy)] pub(crate) enum Form { diff --git a/dhall/src/core/valuef.rs b/dhall/src/semantics/core/valuef.rs index e5d0807..73c715a 100644 --- a/dhall/src/core/valuef.rs +++ b/dhall/src/semantics/core/valuef.rs @@ -1,15 +1,15 @@ use std::collections::HashMap; -use dhall_syntax::{ +use crate::semantics::core::value::{ToExprOptions, Value}; +use crate::semantics::core::var::{AlphaLabel, AlphaVar, Shift, Subst}; +use crate::semantics::phase::typecheck::rc; +use crate::semantics::phase::{Normalized, NormalizedExpr}; +use crate::syntax; +use crate::syntax::{ Builtin, Const, ExprF, Integer, InterpolatedTextContents, Label, NaiveDouble, Natural, }; -use crate::core::value::{ToExprOptions, Value}; -use crate::core::var::{AlphaLabel, AlphaVar, Shift, Subst}; -use crate::phase::typecheck::rc; -use crate::phase::{Normalized, NormalizedExpr}; - /// A semantic value. Subexpressions are Values, which are partially evaluated expressions that are /// normalized on-demand. /// If you compare for equality two `ValueF`s in WHNF, then equality will be up to @@ -117,7 +117,7 @@ impl ValueF { .collect(), )), ValueF::Equivalence(x, y) => rc(ExprF::BinOp( - dhall_syntax::BinOp::Equivalence, + syntax::BinOp::Equivalence, x.to_expr(opts), y.to_expr(opts), )), diff --git a/dhall/src/core/var.rs b/dhall/src/semantics/core/var.rs index 3795f10..184a372 100644 --- a/dhall/src/core/var.rs +++ b/dhall/src/semantics/core/var.rs @@ -1,6 +1,6 @@ use std::collections::HashMap; -use dhall_syntax::{Label, V}; +use crate::syntax::{ExprF, InterpolatedTextContents, Label, V}; /// Stores a pair of variables: a normal one and one /// that corresponds to the alpha-normalized version of the first one. @@ -190,7 +190,7 @@ impl<T: Shift> Shift for std::cell::RefCell<T> { } } -impl<T: Shift, E: Clone> Shift for dhall_syntax::ExprF<T, E> { +impl<T: Shift, E: Clone> Shift for ExprF<T, E> { fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> { Some(self.traverse_ref_with_special_handling_of_binders( |v| Ok(v.shift(delta, var)?), @@ -222,7 +222,7 @@ where } } -impl<T: Shift> Shift for dhall_syntax::InterpolatedTextContents<T> { +impl<T: Shift> Shift for InterpolatedTextContents<T> { fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> { Some(self.traverse_ref(|x| Ok(x.shift(delta, var)?))?) } @@ -262,7 +262,7 @@ impl<S, T: Subst<S>> Subst<S> for std::cell::RefCell<T> { } } -impl<S: Shift, T: Subst<S>, E: Clone> Subst<S> for dhall_syntax::ExprF<T, E> { +impl<S: Shift, T: Subst<S>, E: Clone> Subst<S> for ExprF<T, E> { fn subst_shift(&self, var: &AlphaVar, val: &S) -> Self { self.map_ref_with_special_handling_of_binders( |v| v.subst_shift(var, val), @@ -277,7 +277,7 @@ impl<S, T: Subst<S>> Subst<S> for Vec<T> { } } -impl<S, T: Subst<S>> Subst<S> for dhall_syntax::InterpolatedTextContents<T> { +impl<S, T: Subst<S>> Subst<S> for InterpolatedTextContents<T> { fn subst_shift(&self, var: &AlphaVar, val: &S) -> Self { self.map_ref(|x| x.subst_shift(var, val)) } diff --git a/dhall/src/error/mod.rs b/dhall/src/semantics/error/mod.rs index e4baea0..1288c12 100644 --- a/dhall/src/error/mod.rs +++ b/dhall/src/semantics/error/mod.rs @@ -1,11 +1,10 @@ use std::io::Error as IOError; -use dhall_syntax::{BinOp, Import, Label, ParseError, Span}; - -use crate::core::context::TypecheckContext; -use crate::core::value::Value; -use crate::phase::resolve::ImportStack; -use crate::phase::NormalizedExpr; +use crate::semantics::core::context::TypecheckContext; +use crate::semantics::core::value::Value; +use crate::semantics::phase::resolve::ImportStack; +use crate::semantics::phase::NormalizedExpr; +use crate::syntax::{BinOp, Import, Label, ParseError, Span}; pub type Result<T> = std::result::Result<T, Error>; diff --git a/dhall/src/semantics/mod.rs b/dhall/src/semantics/mod.rs new file mode 100644 index 0000000..9d2e462 --- /dev/null +++ b/dhall/src/semantics/mod.rs @@ -0,0 +1,3 @@ +pub mod core; +pub mod error; +pub mod phase; diff --git a/dhall/src/phase/mod.rs b/dhall/src/semantics/phase/mod.rs index 337ce3d..752c257 100644 --- a/dhall/src/phase/mod.rs +++ b/dhall/src/semantics/phase/mod.rs @@ -1,16 +1,14 @@ use std::fmt::Display; use std::path::Path; -use dhall_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::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; @@ -62,7 +60,7 @@ impl Parsed { } pub fn encode(&self) -> Result<Vec<u8>, EncodeError> { - crate::phase::binary::encode(&self.0) + binary::encode(&self.0) } } @@ -172,7 +170,7 @@ impl Typed { impl Normalized { pub fn encode(&self) -> Result<Vec<u8>, EncodeError> { - crate::phase::binary::encode(&self.to_expr()) + binary::encode(&self.to_expr()) } pub(crate) fn to_expr(&self) -> NormalizedExpr { diff --git a/dhall/src/phase/normalize.rs b/dhall/src/semantics/phase/normalize.rs index b712027..81c3ce1 100644 --- a/dhall/src/phase/normalize.rs +++ b/dhall/src/semantics/phase/normalize.rs @@ -1,21 +1,21 @@ use std::collections::HashMap; -use dhall_syntax::Const::Type; -use dhall_syntax::{ +use crate::semantics::core::value::Value; +use crate::semantics::core::valuef::ValueF; +use crate::semantics::core::var::{AlphaLabel, AlphaVar, Shift, Subst}; +use crate::semantics::phase::Normalized; +use crate::syntax; +use crate::syntax::Const::Type; +use crate::syntax::{ BinOp, Builtin, ExprF, InterpolatedText, InterpolatedTextContents, Label, NaiveDouble, }; -use crate::core::value::Value; -use crate::core::valuef::ValueF; -use crate::core::var::{AlphaLabel, Shift, Subst}; -use crate::phase::Normalized; - // Ad-hoc macro to help construct closures macro_rules! make_closure { (#$var:ident) => { $var.clone() }; (var($var:ident, $n:expr, $($ty:tt)*)) => {{ - let var = crate::core::var::AlphaVar::from_var_and_alpha( + let var = AlphaVar::from_var_and_alpha( Label::from(stringify!($var)).into(), $n ); @@ -47,7 +47,7 @@ macro_rules! make_closure { }}; (1 + $($rest:tt)*) => { ValueF::PartialExpr(ExprF::BinOp( - dhall_syntax::BinOp::NaturalPlus, + syntax::BinOp::NaturalPlus, make_closure!($($rest)*), Value::from_valuef_and_type( ValueF::NaturalLit(1), @@ -62,7 +62,7 @@ macro_rules! make_closure { let tail = make_closure!($($tail)*); let list_type = tail.get_type_not_sort(); ValueF::PartialExpr(ExprF::BinOp( - dhall_syntax::BinOp::ListAppend, + syntax::BinOp::ListAppend, ValueF::NEListLit(vec![head]) .into_value_with_type(list_type.clone()), tail, @@ -76,7 +76,7 @@ pub(crate) fn apply_builtin( args: Vec<Value>, ty: &Value, ) -> ValueF { - use dhall_syntax::Builtin::*; + use syntax::Builtin::*; use ValueF::*; // Small helper enum diff --git a/dhall/src/phase/parse.rs b/dhall/src/semantics/phase/parse.rs index 540ceea..4c8ad7b 100644 --- a/dhall/src/phase/parse.rs +++ b/dhall/src/semantics/phase/parse.rs @@ -2,11 +2,11 @@ use std::fs::File; use std::io::Read; use std::path::Path; -use dhall_syntax::parse_expr; - -use crate::error::Error; -use crate::phase::resolve::ImportRoot; -use crate::phase::Parsed; +use crate::semantics::error::Error; +use crate::semantics::phase::resolve::ImportRoot; +use crate::semantics::phase::Parsed; +use crate::syntax::binary; +use crate::syntax::parse_expr; pub(crate) fn parse_file(f: &Path) -> Result<Parsed, Error> { let mut buffer = String::new(); @@ -23,7 +23,7 @@ pub(crate) fn parse_str(s: &str) -> Result<Parsed, Error> { } pub(crate) fn parse_binary(data: &[u8]) -> Result<Parsed, Error> { - let expr = crate::phase::binary::decode(data)?; + let expr = binary::decode(data)?; let root = ImportRoot::LocalDir(std::env::current_dir()?); Ok(Parsed(expr, root)) } @@ -31,7 +31,7 @@ pub(crate) fn parse_binary(data: &[u8]) -> Result<Parsed, Error> { pub(crate) fn parse_binary_file(f: &Path) -> Result<Parsed, Error> { let mut buffer = Vec::new(); File::open(f)?.read_to_end(&mut buffer)?; - let expr = crate::phase::binary::decode(&buffer)?; + let expr = binary::decode(&buffer)?; let root = ImportRoot::LocalDir(f.parent().unwrap().to_owned()); Ok(Parsed(expr, root)) } diff --git a/dhall/src/phase/resolve.rs b/dhall/src/semantics/phase/resolve.rs index c302bfa..86dc7ae 100644 --- a/dhall/src/phase/resolve.rs +++ b/dhall/src/semantics/phase/resolve.rs @@ -1,11 +1,12 @@ use std::collections::HashMap; use std::path::{Path, PathBuf}; -use crate::error::{Error, ImportError}; -use crate::phase::{Normalized, NormalizedExpr, Parsed, Resolved}; -use dhall_syntax::{FilePath, ImportLocation, URL}; +use crate::semantics::error::{Error, ImportError}; +use crate::semantics::phase::{Normalized, NormalizedExpr, Parsed, Resolved}; +use crate::syntax; +use crate::syntax::{FilePath, ImportLocation, URL}; -type Import = dhall_syntax::Import<NormalizedExpr>; +type Import = syntax::Import<NormalizedExpr>; /// A root from which to resolve relative imports. #[derive(Debug, Clone, PartialEq, Eq)] @@ -24,8 +25,8 @@ fn resolve_import( import_stack: &ImportStack, ) -> Result<Normalized, ImportError> { use self::ImportRoot::*; - use dhall_syntax::FilePrefix::*; - use dhall_syntax::ImportLocation::*; + use syntax::FilePrefix::*; + use syntax::ImportLocation::*; let cwd = match root { LocalDir(cwd) => cwd, }; diff --git a/dhall/src/phase/typecheck.rs b/dhall/src/semantics/phase/typecheck.rs index ef8340d..59380a3 100644 --- a/dhall/src/phase/typecheck.rs +++ b/dhall/src/semantics/phase/typecheck.rs @@ -1,24 +1,25 @@ use std::cmp::max; use std::collections::HashMap; -use dhall_syntax::{ +use crate::semantics::core::context::TypecheckContext; +use crate::semantics::core::value::Value; +use crate::semantics::core::valuef::ValueF; +use crate::semantics::core::var::{Shift, Subst}; +use crate::semantics::error::{TypeError, TypeMessage}; +use crate::semantics::phase::normalize::merge_maps; +use crate::semantics::phase::Normalized; +use crate::syntax; +use crate::syntax::{ Builtin, Const, Expr, ExprF, InterpolatedTextContents, Label, RawExpr, Span, }; -use crate::core::context::TypecheckContext; -use crate::core::value::Value; -use crate::core::valuef::ValueF; -use crate::core::var::{Shift, Subst}; -use crate::error::{TypeError, TypeMessage}; -use crate::phase::Normalized; - fn tck_pi_type( ctx: &TypecheckContext, x: Label, tx: Value, te: Value, ) -> Result<Value, TypeError> { - use crate::error::TypeMessage::*; + use TypeMessage::*; let ctx2 = ctx.insert_type(&x, tx.clone()); let ka = match tx.get_type()?.as_const() { @@ -48,8 +49,8 @@ fn tck_record_type( ctx: &TypecheckContext, kts: impl IntoIterator<Item = Result<(Label, Value), TypeError>>, ) -> Result<Value, TypeError> { - use crate::error::TypeMessage::*; use std::collections::hash_map::Entry; + use TypeMessage::*; let mut new_kts = HashMap::new(); // An empty record type has type Type let mut k = Const::Type; @@ -83,8 +84,8 @@ fn tck_union_type<Iter>( where Iter: IntoIterator<Item = Result<(Label, Option<Value>), TypeError>>, { - use crate::error::TypeMessage::*; use std::collections::hash_map::Entry; + use TypeMessage::*; let mut new_kts = HashMap::new(); // Check that all types are the same const let mut k = None; @@ -155,7 +156,7 @@ macro_rules! make_type { (Double) => { ExprF::Builtin(Builtin::Double) }; (Text) => { ExprF::Builtin(Builtin::Text) }; ($var:ident) => { - ExprF::Var(dhall_syntax::V(stringify!($var).into(), 0)) + ExprF::Var(syntax::V(stringify!($var).into(), 0)) }; (Optional $ty:ident) => { ExprF::App( @@ -170,7 +171,7 @@ macro_rules! make_type { ) }; ({ $($label:ident : $ty:ident),* }) => {{ - let mut kts = dhall_syntax::map::DupTreeMap::new(); + let mut kts = syntax::map::DupTreeMap::new(); $( kts.insert( Label::from(stringify!($label)), @@ -203,7 +204,7 @@ macro_rules! make_type { } fn type_of_builtin<E>(b: Builtin) -> Expr<E> { - use dhall_syntax::Builtin::*; + use syntax::Builtin::*; rc(match b { Bool | Natural | Integer | Double | Text => make_type!(Type), List | Optional => make_type!( @@ -303,7 +304,7 @@ fn type_with( ctx: &TypecheckContext, e: Expr<Normalized>, ) -> Result<Value, TypeError> { - use dhall_syntax::ExprF::{Annot, Embed, Lam, Let, Pi, Var}; + use syntax::ExprF::{Annot, Embed, Lam, Let, Pi, Var}; let span = e.span(); Ok(match e.as_ref() { @@ -361,11 +362,11 @@ fn type_last_layer( e: ExprF<Value, Normalized>, span: Span, ) -> Result<Value, TypeError> { - use crate::error::TypeMessage::*; - use dhall_syntax::BinOp::*; - use dhall_syntax::Builtin::*; - use dhall_syntax::Const::Type; - use dhall_syntax::ExprF::*; + use syntax::BinOp::*; + use syntax::Builtin::*; + use syntax::Const::Type; + use syntax::ExprF::*; + use TypeMessage::*; let mkerr = |msg: TypeMessage| Err(TypeError::new(ctx, msg)); /// Intermediary return type @@ -434,7 +435,7 @@ fn type_last_layer( } EmptyListLit(t) => { match &*t.as_whnf() { - ValueF::AppliedBuiltin(dhall_syntax::Builtin::List, args) + ValueF::AppliedBuiltin(syntax::Builtin::List, args) if args.len() == 1 => {} _ => return mkerr(InvalidListType(t.clone())), } @@ -457,7 +458,7 @@ fn type_last_layer( return mkerr(InvalidListType(t)); } - RetTypeOnly(Value::from_builtin(dhall_syntax::Builtin::List).app(t)) + RetTypeOnly(Value::from_builtin(syntax::Builtin::List).app(t)) } SomeLit(x) => { let t = x.get_type()?; @@ -465,9 +466,7 @@ fn type_last_layer( return mkerr(InvalidOptionalType(t)); } - RetTypeOnly( - Value::from_builtin(dhall_syntax::Builtin::Optional).app(t), - ) + RetTypeOnly(Value::from_builtin(syntax::Builtin::Optional).app(t)) } RecordType(kts) => RetWhole(tck_record_type( ctx, @@ -548,8 +547,6 @@ fn type_last_layer( RetTypeOnly(text_type) } BinOp(RightBiasedRecordMerge, l, r) => { - use crate::phase::normalize::merge_maps; - let l_type = l.get_type()?; let r_type = r.get_type()?; @@ -589,8 +586,6 @@ fn type_last_layer( Span::Artificial, )?), BinOp(RecursiveRecordTypeMerge, l, r) => { - use crate::phase::normalize::merge_maps; - // Extract the LHS record type let borrow_l = l.as_whnf(); let kts_x = match &*borrow_l { |