summaryrefslogtreecommitdiff
path: root/dhall
diff options
context:
space:
mode:
authorNadrieril2019-08-13 22:11:45 +0200
committerNadrieril2019-08-13 22:11:45 +0200
commit8d45d633dfa60e8d64c9e6e742de4e33496bf0fa (patch)
tree526c351bbdd6121cdde3cd56f721156d3b34e6de /dhall
parent07956ccb1daf4a6819f64776f70b6f5f26869184 (diff)
Store Imports in their own node instead of in Embed
Diffstat (limited to 'dhall')
-rw-r--r--dhall/src/phase/binary.rs24
-rw-r--r--dhall/src/phase/mod.rs8
-rw-r--r--dhall/src/phase/normalize.rs3
-rw-r--r--dhall/src/phase/typecheck.rs3
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!()
}