diff options
Diffstat (limited to 'dhall')
-rw-r--r-- | dhall/src/phase/binary.rs | 24 | ||||
-rw-r--r-- | dhall/src/phase/mod.rs | 8 | ||||
-rw-r--r-- | dhall/src/phase/normalize.rs | 3 | ||||
-rw-r--r-- | dhall/src/phase/typecheck.rs | 3 |
4 files changed, 25 insertions, 13 deletions
diff --git a/dhall/src/phase/binary.rs b/dhall/src/phase/binary.rs index 3292617..b3a80aa 100644 --- a/dhall/src/phase/binary.rs +++ b/dhall/src/phase/binary.rs @@ -19,7 +19,6 @@ pub fn decode(data: &[u8]) -> Result<DecodedSubExpr, DecodeError> { } } -//TODO: encode normalized expression too pub fn encode(expr: &ParsedSubExpr) -> Result<Vec<u8>, EncodeError> { serde_cbor::ser::to_vec(&Serialize::Expr(expr)) .map_err(|e| EncodeError::CBORError(e)) @@ -264,7 +263,7 @@ fn cbor_value_to_dhall( // TODO // Some(x) => { // match cbor_value_to_dhall(&x)?.as_ref() { - // Embed(import) => Some(Box::new( + // Import(import) => Some(Box::new( // import.location_hashed.clone(), // )), // _ => Err(DecodeError::WrongFormatError( @@ -340,7 +339,7 @@ fn cbor_value_to_dhall( "import/type".to_owned(), ))?, }; - Embed(Import { + Import(dhall_syntax::Import { mode, location_hashed: ImportHashed { hash, location }, }) @@ -573,7 +572,10 @@ 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" + ), } } @@ -631,12 +633,14 @@ where 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(location_hashed) => { + ser_seq.serialize_element(&self::Serialize::Expr(&rc( + ExprF::Import(dhall_syntax::Import { + mode: ImportMode::Code, + location_hashed: location_hashed.as_ref().clone(), + }), + )))? + } }; ser_seq.serialize_element(&url.authority)?; for p in &url.path { diff --git a/dhall/src/phase/mod.rs b/dhall/src/phase/mod.rs index 7364949..a1e3f29 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}; +use dhall_syntax::{Const, SubExpr, Void}; use crate::core::thunk::{Thunk, TypedThunk}; use crate::core::value::Value; @@ -17,8 +17,8 @@ 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<Normalized>; @@ -26,6 +26,8 @@ pub type NormalizedSubExpr = SubExpr<Normalized>; 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); diff --git a/dhall/src/phase/normalize.rs b/dhall/src/phase/normalize.rs index 2970f5f..adbcb02 100644 --- a/dhall/src/phase/normalize.rs +++ b/dhall/src/phase/normalize.rs @@ -644,6 +644,9 @@ pub fn normalize_one_layer(expr: ExprF<Thunk, Normalized>) -> 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/typecheck.rs b/dhall/src/phase/typecheck.rs index e8b2544..89e2da8 100644 --- a/dhall/src/phase/typecheck.rs +++ b/dhall/src/phase/typecheck.rs @@ -407,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!() } |