diff options
author | Nadrieril Feneanar | 2019-08-14 00:09:14 +0200 |
---|---|---|
committer | GitHub | 2019-08-14 00:09:14 +0200 |
commit | 160b05778808976ab9bd79fa7a142ca2e94ac67a (patch) | |
tree | b3094a3d4e6b463724302b9be7e803a80ce4eed3 /dhall/src | |
parent | 5895c3aa6552f75d7e5202be561f9734fe8945e7 (diff) | |
parent | 66260f8e386f7a447352bd8ccbda064b00b698bc (diff) |
Merge pull request #102 from Nadrieril/inline-headers
Implement inline headers parsing
Diffstat (limited to 'dhall/src')
-rw-r--r-- | dhall/src/core/thunk.rs | 10 | ||||
-rw-r--r-- | dhall/src/core/value.rs | 14 | ||||
-rw-r--r-- | dhall/src/error/mod.rs | 8 | ||||
-rw-r--r-- | dhall/src/phase/binary.rs | 91 | ||||
-rw-r--r-- | dhall/src/phase/mod.rs | 26 | ||||
-rw-r--r-- | dhall/src/phase/normalize.rs | 25 | ||||
-rw-r--r-- | dhall/src/phase/resolve.rs | 8 | ||||
-rw-r--r-- | dhall/src/phase/typecheck.rs | 17 |
8 files changed, 101 insertions, 98 deletions
diff --git a/dhall/src/core/thunk.rs b/dhall/src/core/thunk.rs index c18014e..7c5c537 100644 --- a/dhall/src/core/thunk.rs +++ b/dhall/src/core/thunk.rs @@ -2,7 +2,7 @@ use std::borrow::Cow; use std::cell::{Ref, RefCell}; use std::rc::Rc; -use dhall_syntax::{Const, ExprF, X}; +use dhall_syntax::{Const, ExprF}; use crate::core::context::{NormalizationContext, TypecheckContext}; use crate::core::value::Value; @@ -12,7 +12,7 @@ use crate::phase::normalize::{ apply_any, normalize_one_layer, normalize_whnf, InputSubExpr, OutputSubExpr, }; use crate::phase::typecheck::type_of_const; -use crate::phase::{NormalizedSubExpr, Type, Typed}; +use crate::phase::{Normalized, NormalizedSubExpr, Type, Typed}; #[derive(Debug, Clone, Copy)] enum Marker { @@ -30,7 +30,7 @@ enum ThunkInternal { /// Partially normalized value whose subexpressions have been thunked (this is returned from /// typechecking). Note that this is different from `Value::PartialExpr` because there is no /// requirement of WHNF here. - PartialExpr(ExprF<Thunk, X>), + PartialExpr(ExprF<Thunk, Normalized>), /// Partially normalized value. /// Invariant: if the marker is `NF`, the value must be fully normalized Value(Marker, Value), @@ -123,7 +123,7 @@ impl Thunk { ThunkInternal::Value(WHNF, v).into_thunk() } - pub fn from_partial_expr(e: ExprF<Thunk, X>) -> Thunk { + pub fn from_partial_expr(e: ExprF<Thunk, Normalized>) -> Thunk { ThunkInternal::PartialExpr(e).into_thunk() } @@ -309,7 +309,6 @@ impl Shift for ThunkInternal { e.traverse_ref_with_special_handling_of_binders( |v| Ok(v.shift(delta, var)?), |x, v| Ok(v.shift(delta, &var.under_binder(x))?), - |x| Ok(X::clone(x)), )?, ), ThunkInternal::Value(m, v) => { @@ -356,7 +355,6 @@ impl Subst<Typed> for ThunkInternal { &val.under_binder(x), ) }, - X::clone, ), ), ThunkInternal::Value(_, v) => { diff --git a/dhall/src/core/value.rs b/dhall/src/core/value.rs index 8486d6e..20a6021 100644 --- a/dhall/src/core/value.rs +++ b/dhall/src/core/value.rs @@ -2,7 +2,7 @@ use std::collections::HashMap; use dhall_syntax::{ rc, Builtin, Const, ExprF, Integer, InterpolatedTextContents, Label, - NaiveDouble, Natural, X, + NaiveDouble, Natural, }; use crate::core::thunk::{Thunk, TypedThunk}; @@ -10,7 +10,7 @@ use crate::core::var::{AlphaLabel, AlphaVar, Shift, Subst}; use crate::phase::normalize::{ apply_builtin, normalize_one_layer, squash_textlit, OutputSubExpr, }; -use crate::phase::Typed; +use crate::phase::{Normalized, Typed}; /// A semantic value. The invariants ensure this value represents a Weak-Head /// Normal Form (WHNF). This means that this first constructor is the first constructor of the @@ -59,7 +59,7 @@ pub enum Value { TextLit(Vec<InterpolatedTextContents<Thunk>>), Equivalence(TypedThunk, TypedThunk), // Invariant: this must not contain a value captured by one of the variants above. - PartialExpr(ExprF<Thunk, X>), + PartialExpr(ExprF<Thunk, Normalized>), } impl Value { @@ -243,7 +243,7 @@ impl Value { y.normalize_to_expr_maybe_alpha(alpha), )), Value::PartialExpr(e) => { - rc(e.map_ref_simple(|v| v.normalize_to_expr_maybe_alpha(alpha))) + rc(e.map_ref(|v| v.normalize_to_expr_maybe_alpha(alpha))) } } } @@ -333,8 +333,8 @@ impl Value { y.normalize_mut(); } Value::PartialExpr(e) => { - // TODO: need map_mut_simple - e.map_ref_simple(|v| { + // TODO: need map_mut + e.map_ref(|v| { v.normalize_nf(); }); } @@ -475,7 +475,6 @@ impl Shift for Value { e.traverse_ref_with_special_handling_of_binders( |v| Ok(v.shift(delta, var)?), |x, v| Ok(v.shift(delta, &var.under_binder(x))?), - |x| Ok(X::clone(x)), )?, ), }) @@ -500,7 +499,6 @@ impl Subst<Typed> for Value { &val.under_binder(x), ) }, - X::clone, )) } // Retry normalizing since substituting may allow progress diff --git a/dhall/src/error/mod.rs b/dhall/src/error/mod.rs index 3626d96..8f6ff51 100644 --- a/dhall/src/error/mod.rs +++ b/dhall/src/error/mod.rs @@ -4,7 +4,7 @@ use dhall_syntax::{BinOp, Import, Label, ParseError, V}; use crate::core::context::TypecheckContext; use crate::phase::resolve::ImportStack; -use crate::phase::{Normalized, Type, Typed}; +use crate::phase::{Normalized, NormalizedSubExpr, Type, Typed}; pub type Result<T> = std::result::Result<T, Error>; @@ -21,9 +21,9 @@ pub enum Error { #[derive(Debug)] pub enum ImportError { - Recursive(Import, Box<Error>), - UnexpectedImport(Import), - ImportCycle(ImportStack, Import), + Recursive(Import<NormalizedSubExpr>, Box<Error>), + UnexpectedImport(Import<NormalizedSubExpr>), + ImportCycle(ImportStack, Import<NormalizedSubExpr>), } #[derive(Debug)] diff --git a/dhall/src/phase/binary.rs b/dhall/src/phase/binary.rs index 3292617..36dd471 100644 --- a/dhall/src/phase/binary.rs +++ b/dhall/src/phase/binary.rs @@ -4,13 +4,12 @@ use std::iter::FromIterator; use dhall_syntax::map::DupTreeMap; use dhall_syntax::{ - rc, ExprF, FilePrefix, Hash, Import, ImportHashed, ImportLocation, - ImportMode, Integer, InterpolatedText, Label, Natural, Scheme, SubExpr, - URL, V, + rc, ExprF, FilePrefix, Hash, Import, ImportLocation, ImportMode, Integer, + InterpolatedText, Label, Natural, Scheme, SubExpr, URL, V, }; use crate::error::{DecodeError, EncodeError}; -use crate::phase::{DecodedSubExpr, ParsedSubExpr}; +use crate::phase::DecodedSubExpr; pub fn decode(data: &[u8]) -> Result<DecodedSubExpr, DecodeError> { match serde_cbor::de::from_slice(data) { @@ -19,8 +18,7 @@ pub fn decode(data: &[u8]) -> Result<DecodedSubExpr, DecodeError> { } } -//TODO: encode normalized expression too -pub fn encode(expr: &ParsedSubExpr) -> Result<Vec<u8>, EncodeError> { +pub fn encode<E>(expr: &SubExpr<E>) -> Result<Vec<u8>, EncodeError> { serde_cbor::ser::to_vec(&Serialize::Expr(expr)) .map_err(|e| EncodeError::CBORError(e)) } @@ -261,20 +259,12 @@ fn cbor_value_to_dhall( }; let headers = match rest.next() { Some(Null) => None, - // TODO - // Some(x) => { - // match cbor_value_to_dhall(&x)?.as_ref() { - // Embed(import) => Some(Box::new( - // import.location_hashed.clone(), - // )), - // _ => Err(DecodeError::WrongFormatError( - // "import/remote/headers".to_owned(), - // ))?, - // } - // } + Some(x) => { + let x = cbor_value_to_dhall(&x)?; + Some(x) + } _ => Err(DecodeError::WrongFormatError( - "import/remote/headers is unimplemented" - .to_owned(), + "import/remote/headers".to_owned(), ))?, }; let authority = match rest.next() { @@ -340,9 +330,10 @@ fn cbor_value_to_dhall( "import/type".to_owned(), ))?, }; - Embed(Import { + Import(dhall_syntax::Import { mode, - location_hashed: ImportHashed { hash, location }, + hash, + location, }) } [U64(25), bindings..] => { @@ -424,11 +415,11 @@ where .collect::<Result<_, _>>() } -enum Serialize<'a> { - Expr(&'a ParsedSubExpr), +enum Serialize<'a, E> { + Expr(&'a SubExpr<E>), CBOR(cbor::Value), - RecordMap(&'a DupTreeMap<Label, ParsedSubExpr>), - UnionMap(&'a DupTreeMap<Label, Option<ParsedSubExpr>>), + RecordMap(&'a DupTreeMap<Label, SubExpr<E>>), + UnionMap(&'a DupTreeMap<Label, Option<SubExpr<E>>>), } macro_rules! count { @@ -448,7 +439,7 @@ macro_rules! ser_seq { }}; } -fn serialize_subexpr<S>(ser: S, e: &ParsedSubExpr) -> Result<S::Ok, S::Error> +fn serialize_subexpr<S, E>(ser: S, e: &SubExpr<E>) -> Result<S::Ok, S::Error> where S: serde::ser::Serializer, { @@ -458,21 +449,14 @@ where use std::iter::once; use self::Serialize::{RecordMap, UnionMap}; - fn expr(x: &ParsedSubExpr) -> self::Serialize<'_> { + fn expr<E>(x: &SubExpr<E>) -> self::Serialize<'_, E> { self::Serialize::Expr(x) } - fn cbor<'a>(v: cbor::Value) -> self::Serialize<'a> { - self::Serialize::CBOR(v) - } - fn tag<'a>(x: u64) -> self::Serialize<'a> { - cbor(U64(x)) - } - fn null<'a>() -> self::Serialize<'a> { - cbor(cbor::Value::Null) - } - fn label<'a>(l: &Label) -> self::Serialize<'a> { - cbor(cbor::Value::String(l.into())) - } + let cbor = + |v: cbor::Value| -> self::Serialize<'_, E> { self::Serialize::CBOR(v) }; + let tag = |x: u64| cbor(U64(x)); + let null = || cbor(cbor::Value::Null); + let label = |l: &Label| cbor(cbor::Value::String(l.into())); match e.as_ref() { Const(c) => ser.serialize_str(&c.to_string()), @@ -573,18 +557,24 @@ where .chain(once(expr(x))) .chain(ls.iter().map(label)), ), - Embed(import) => serialize_import(ser, import), + Import(import) => serialize_import(ser, import), + Embed(_) => unimplemented!( + "An expression with resolved imports cannot be binary-encoded" + ), } } -fn serialize_import<S>(ser: S, import: &Import) -> Result<S::Ok, S::Error> +fn serialize_import<S, E>( + ser: S, + import: &Import<SubExpr<E>>, +) -> Result<S::Ok, S::Error> where S: serde::ser::Serializer, { use cbor::Value::{Bytes, Null, U64}; use serde::ser::SerializeSeq; - let count = 4 + match &import.location_hashed.location { + let count = 4 + match &import.location { ImportLocation::Remote(url) => 3 + url.path.len(), ImportLocation::Local(_, path) => path.len(), ImportLocation::Env(_) => 1, @@ -594,7 +584,7 @@ where ser_seq.serialize_element(&U64(24))?; - let hash = match &import.location_hashed.hash { + let hash = match &import.hash { None => Null, Some(Hash::SHA256(h)) => { let mut bytes = vec![18, 32]; @@ -611,7 +601,7 @@ where }; ser_seq.serialize_element(&U64(mode))?; - let scheme = match &import.location_hashed.location { + let scheme = match &import.location { ImportLocation::Remote(url) => match url.scheme { Scheme::HTTP => 0, Scheme::HTTPS => 1, @@ -627,16 +617,13 @@ where }; ser_seq.serialize_element(&U64(scheme))?; - match &import.location_hashed.location { + match &import.location { ImportLocation::Remote(url) => { match &url.headers { None => ser_seq.serialize_element(&Null)?, - Some(location_hashed) => ser_seq.serialize_element( - &self::Serialize::Expr(&rc(ExprF::Embed(Import { - mode: ImportMode::Code, - location_hashed: location_hashed.as_ref().clone(), - }))), - )?, + Some(e) => { + ser_seq.serialize_element(&self::Serialize::Expr(e))? + } }; ser_seq.serialize_element(&url.authority)?; for p in &url.path { @@ -661,7 +648,7 @@ where ser_seq.end() } -impl<'a> serde::ser::Serialize for Serialize<'a> { +impl<'a, E> serde::ser::Serialize for Serialize<'a, E> { fn serialize<S>(&self, ser: S) -> Result<S::Ok, S::Error> where S: serde::ser::Serializer, diff --git a/dhall/src/phase/mod.rs b/dhall/src/phase/mod.rs index 8c93889..b73597c 100644 --- a/dhall/src/phase/mod.rs +++ b/dhall/src/phase/mod.rs @@ -2,7 +2,7 @@ use std::borrow::Cow; use std::fmt::Display; use std::path::Path; -use dhall_syntax::{Const, Import, SubExpr, X}; +use dhall_syntax::{Const, SubExpr, Void}; use crate::core::thunk::{Thunk, TypedThunk}; use crate::core::value::Value; @@ -17,15 +17,17 @@ pub(crate) mod parse; pub(crate) mod resolve; pub(crate) mod typecheck; -pub type ParsedSubExpr = SubExpr<Import>; -pub type DecodedSubExpr = SubExpr<Import>; +pub type ParsedSubExpr = SubExpr<Void>; +pub type DecodedSubExpr = SubExpr<Void>; pub type ResolvedSubExpr = SubExpr<Normalized>; -pub type NormalizedSubExpr = SubExpr<X>; +pub type NormalizedSubExpr = SubExpr<Normalized>; #[derive(Debug, Clone)] pub struct Parsed(ParsedSubExpr, 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(ResolvedSubExpr); @@ -155,6 +157,10 @@ impl Typed { } impl Normalized { + pub fn encode(&self) -> Result<Vec<u8>, EncodeError> { + crate::phase::binary::encode(&self.to_expr()) + } + #[allow(dead_code)] pub fn to_expr(&self) -> NormalizedSubExpr { self.0.to_expr() @@ -218,6 +224,18 @@ 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<H>(&self, state: &mut H) + where + H: std::hash::Hasher, + { + match self.encode() { + Ok(vec) => vec.hash(state), + Err(_) => {} + } + } +} + impl Eq for Typed {} impl PartialEq for Typed { fn eq(&self, other: &Self) -> bool { diff --git a/dhall/src/phase/normalize.rs b/dhall/src/phase/normalize.rs index 644f98c..adbcb02 100644 --- a/dhall/src/phase/normalize.rs +++ b/dhall/src/phase/normalize.rs @@ -2,14 +2,14 @@ use std::collections::HashMap; use dhall_syntax::{ BinOp, Builtin, ExprF, InterpolatedText, InterpolatedTextContents, - NaiveDouble, X, + NaiveDouble, }; use crate::core::context::NormalizationContext; use crate::core::thunk::{Thunk, TypedThunk}; use crate::core::value::Value; use crate::core::var::Subst; -use crate::phase::{NormalizedSubExpr, ResolvedSubExpr, Typed}; +use crate::phase::{Normalized, NormalizedSubExpr, ResolvedSubExpr, Typed}; pub type InputSubExpr = ResolvedSubExpr; pub type OutputSubExpr = NormalizedSubExpr; @@ -86,7 +86,7 @@ pub fn apply_builtin(b: Builtin, args: Vec<Thunk>) -> Value { // Empty string literal. [] => { // Printing InterpolatedText takes care of all the escaping - let txt: InterpolatedText<X> = + let txt: InterpolatedText<Normalized> = std::iter::empty().collect(); let s = txt.to_string(); Ok(( @@ -98,10 +98,11 @@ pub fn apply_builtin(b: Builtin, args: Vec<Thunk>) -> Value { // interpolations, there is a single Text item) in the literal. [InterpolatedTextContents::Text(s)] => { // Printing InterpolatedText takes care of all the escaping - let txt: InterpolatedText<X> = std::iter::once( - InterpolatedTextContents::Text(s.clone()), - ) - .collect(); + let txt: InterpolatedText<Normalized> = + std::iter::once(InterpolatedTextContents::Text( + s.clone(), + )) + .collect(); let s = txt.to_string(); Ok(( r, @@ -376,11 +377,10 @@ pub fn normalize_whnf(ctx: NormalizationContext, expr: InputSubExpr) -> Value { } // Thunk subexpressions - let expr: ExprF<Thunk, X> = + let expr: ExprF<Thunk, Normalized> = expr.as_ref().map_ref_with_special_handling_of_binders( |e| Thunk::new(ctx.clone(), e.clone()), |x, e| Thunk::new(ctx.skip(x), e.clone()), - |_| unreachable!(), ); normalize_one_layer(expr) @@ -391,7 +391,7 @@ enum Ret<'a> { Value(Value), Thunk(Thunk), ThunkRef(&'a Thunk), - Expr(ExprF<Thunk, X>), + Expr(ExprF<Thunk, Normalized>), } /// Performs an intersection of two HashMaps. @@ -636,7 +636,7 @@ fn apply_binop<'a>(o: BinOp, x: &'a Thunk, y: &'a Thunk) -> Option<Ret<'a>> { }) } -pub fn normalize_one_layer(expr: ExprF<Thunk, X>) -> Value { +pub fn normalize_one_layer(expr: ExprF<Thunk, Normalized>) -> Value { use Value::{ AppliedBuiltin, BoolLit, DoubleLit, EmptyListLit, IntegerLit, Lam, NEListLit, NEOptionalLit, NaturalLit, Pi, RecordLit, RecordType, @@ -644,6 +644,9 @@ pub fn normalize_one_layer(expr: ExprF<Thunk, X>) -> Value { }; let ret = match expr { + ExprF::Import(_) => unreachable!( + "There should remain no imports in a resolved expression" + ), ExprF::Embed(_) => unreachable!(), ExprF::Var(_) => unreachable!(), ExprF::Annot(x, _) => Ret::Thunk(x), diff --git a/dhall/src/phase/resolve.rs b/dhall/src/phase/resolve.rs index abcee7e..52353e4 100644 --- a/dhall/src/phase/resolve.rs +++ b/dhall/src/phase/resolve.rs @@ -1,10 +1,10 @@ use std::collections::HashMap; use std::path::{Path, PathBuf}; -use dhall_syntax::Import; - use crate::error::{Error, ImportError}; -use crate::phase::{Normalized, Parsed, Resolved}; +use crate::phase::{Normalized, NormalizedSubExpr, Parsed, Resolved}; + +type Import = dhall_syntax::Import<NormalizedSubExpr>; /// A root from which to resolve relative imports. #[derive(Debug, Clone, PartialEq, Eq)] @@ -28,7 +28,7 @@ fn resolve_import( let cwd = match root { LocalDir(cwd) => cwd, }; - match &import.location_hashed.location { + match &import.location { Local(prefix, path) => { let path: PathBuf = path.iter().cloned().collect(); let path = match prefix { diff --git a/dhall/src/phase/typecheck.rs b/dhall/src/phase/typecheck.rs index ecf9793..89e2da8 100644 --- a/dhall/src/phase/typecheck.rs +++ b/dhall/src/phase/typecheck.rs @@ -2,7 +2,6 @@ use std::collections::HashMap; use dhall_syntax::{ rc, Builtin, Const, Expr, ExprF, InterpolatedTextContents, Label, SubExpr, - X, }; use crate::core::context::{NormalizationContext, TypecheckContext}; @@ -214,7 +213,7 @@ macro_rules! make_type { }; } -fn type_of_builtin(b: Builtin) -> Expr<X> { +fn type_of_builtin<E>(b: Builtin) -> Expr<E> { use dhall_syntax::Builtin::*; match b { Bool | Natural | Integer | Double | Text => make_type!(Type), @@ -377,12 +376,11 @@ fn type_with( e.as_ref().traverse_ref_with_special_handling_of_binders( |e| type_with(ctx, e.clone()), |_, _| unreachable!(), - |_| unreachable!(), )?; let ret = type_last_layer(ctx, &expr)?; match ret { RetTypeOnly(typ) => { - let expr = expr.map_ref_simple(|typed| typed.to_thunk()); + let expr = expr.map_ref(|typed| typed.to_thunk()); Typed::from_thunk_and_type( Thunk::from_partial_expr(expr), typ, @@ -398,7 +396,7 @@ fn type_with( /// layer. fn type_last_layer( ctx: &TypecheckContext, - e: &ExprF<Typed, X>, + e: &ExprF<Typed, Normalized>, ) -> Result<Ret, TypeError> { use crate::error::TypeMessage::*; use dhall_syntax::BinOp::*; @@ -409,6 +407,9 @@ fn type_last_layer( let mkerr = |msg: TypeMessage| TypeError::new(ctx, msg); match e { + Import(_) => unreachable!( + "There should remain no imports in a resolved expression" + ), Lam(_, _, _) | Pi(_, _, _) | Let(_, _, _, _) | Embed(_) | Var(_) => { unreachable!() } @@ -598,9 +599,7 @@ fn type_last_layer( } } Const(c) => Ok(RetWhole(Typed::from_const(*c))), - Builtin(b) => { - Ok(RetTypeOnly(mktype(ctx, rc(type_of_builtin(*b)).absurd())?)) - } + Builtin(b) => Ok(RetTypeOnly(mktype(ctx, rc(type_of_builtin(*b)))?)), BoolLit(_) => Ok(RetTypeOnly(builtin_to_type(Bool)?)), NaturalLit(_) => Ok(RetTypeOnly(builtin_to_type(Natural)?)), IntegerLit(_) => Ok(RetTypeOnly(builtin_to_type(Integer)?)), @@ -1016,7 +1015,7 @@ pub fn typecheck(e: Resolved) -> Result<Typed, TypeError> { pub fn typecheck_with(e: Resolved, ty: &Type) -> Result<Typed, TypeError> { let expr: SubExpr<_> = e.0; - let ty: SubExpr<_> = ty.to_expr().absurd(); + let ty: SubExpr<_> = ty.to_expr(); type_of(expr.rewrap(ExprF::Annot(expr.clone(), ty))) } pub fn skip_typecheck(e: Resolved) -> Typed { |