summaryrefslogtreecommitdiff
path: root/dhall
diff options
context:
space:
mode:
authorNadrieril2020-04-06 11:48:28 +0100
committerGitHub2020-04-06 11:48:28 +0100
commitd35cb130d80d628807a4247ddf84a8d0230c87ab (patch)
treeb99dadebeab8094c129cc5d872cfd561f9aa78f3 /dhall
parent4290615769fc26c5e4b70843e7fbfddf6359af41 (diff)
parent12b81d55e1343fc30138d1a13cd48fa2e05744df (diff)
Merge pull request #158 from Nadrieril/hash
Implement semantic hashing (but no caching yet)
Diffstat (limited to '')
-rw-r--r--dhall/Cargo.toml1
-rw-r--r--dhall/build.rs31
-rw-r--r--dhall/src/semantics/resolve/env.rs20
-rw-r--r--dhall/src/semantics/resolve/hir.rs4
-rw-r--r--dhall/src/semantics/resolve/resolve.rs43
-rw-r--r--dhall/src/syntax/ast/expr.rs8
-rw-r--r--dhall/src/tests.rs8
-rw-r--r--dhall/tests/import/failure/hashMismatch.txt8
8 files changed, 94 insertions, 29 deletions
diff --git a/dhall/Cargo.toml b/dhall/Cargo.toml
index 75d38f1..ae6665e 100644
--- a/dhall/Cargo.toml
+++ b/dhall/Cargo.toml
@@ -22,6 +22,7 @@ pest_consume = "1.0"
reqwest = { version = "0.10", features = ["blocking"] }
serde = "1.0"
serde_cbor = "0.9.0"
+sha2 = "0.8.1"
smallvec = "1.0.0"
url = "2.1"
diff --git a/dhall/build.rs b/dhall/build.rs
index 19abcc4..784ce93 100644
--- a/dhall/build.rs
+++ b/dhall/build.rs
@@ -14,6 +14,8 @@ enum FileType {
Text,
/// Dhall binary file
Binary,
+ /// Text file with hash
+ Hash,
/// Text file with expected text output
UI,
}
@@ -23,6 +25,7 @@ impl FileType {
match self {
FileType::Text => "dhall",
FileType::Binary => "dhallb",
+ FileType::Hash => "hash",
FileType::UI => "txt",
}
}
@@ -30,6 +33,7 @@ impl FileType {
match self {
FileType::Text => "TestFile::Source",
FileType::Binary => "TestFile::Binary",
+ FileType::Hash => "TestFile::Binary",
FileType::UI => "TestFile::UI",
}
}
@@ -252,9 +256,7 @@ fn generate_tests() -> std::io::Result<()> {
exclude_path: Rc::new(|path: &str| {
false
// TODO: import hash
- || path == "alternativeHashMismatch"
|| path == "hashFromCache"
- || path == "unit/AlternativeHashMismatch"
// TODO: the standard does not respect https://tools.ietf.org/html/rfc3986#section-5.2
|| path == "unit/asLocation/RemoteCanonicalize4"
// TODO: import headers
@@ -271,8 +273,6 @@ fn generate_tests() -> std::io::Result<()> {
variant: "ImportFailure",
exclude_path: Rc::new(|path: &str| {
false
- // TODO: import hash
- || path == "hashMismatch"
// TODO: import headers
|| path == "customHeadersUsingBoundVariable"
}),
@@ -280,6 +280,22 @@ fn generate_tests() -> std::io::Result<()> {
..default_feature.clone()
},
TestFeature {
+ module_name: "semantic_hash",
+ directory: "semantic-hash/success/",
+ variant: "SemanticHash",
+ exclude_path: Rc::new(|path: &str| {
+ false
+ // We don't support bignums
+ || path == "simple/integerToDouble"
+ // See https://github.com/pyfisch/cbor/issues/109
+ || path == "prelude/Integer/toDouble/0"
+ || path == "prelude/Integer/toDouble/1"
+ || path == "prelude/Natural/toDouble/0"
+ }),
+ output_type: Some(FileType::Hash),
+ ..default_feature.clone()
+ },
+ TestFeature {
module_name: "beta_normalize",
directory: "normalization/success/",
variant: "Normalization",
@@ -314,12 +330,7 @@ fn generate_tests() -> std::io::Result<()> {
module_name: "type_inference_success",
directory: "type-inference/success/",
variant: "TypeInferenceSuccess",
- exclude_path: Rc::new(|path: &str| {
- false
- // Too slow, but also not all features implemented
- // For now needs support for hashed imports
- || path == "prelude"
- }),
+ too_slow_path: Rc::new(|path: &str| path == "prelude"),
output_type: Some(FileType::Text),
..default_feature.clone()
},
diff --git a/dhall/src/semantics/resolve/env.rs b/dhall/src/semantics/resolve/env.rs
index d7ff0ae..6346a6d 100644
--- a/dhall/src/semantics/resolve/env.rs
+++ b/dhall/src/semantics/resolve/env.rs
@@ -71,7 +71,7 @@ impl ImportEnv {
pub fn handle_import(
&mut self,
- location: ImportLocation,
+ mut location: ImportLocation,
do_resolve: impl FnOnce(&mut Self) -> Result<TypedHir, Error>,
) -> Result<TypedHir, Error> {
if self.stack.contains(&location) {
@@ -82,14 +82,16 @@ impl ImportEnv {
Ok(match self.cache.get(&location) {
Some(expr) => expr.clone(),
None => {
- // Push the current location on the stack
- self.stack.push(location);
-
- // Resolve the import recursively
- let expr = do_resolve(self)?;
-
- // Remove location from the stack.
- let location = self.stack.pop().unwrap();
+ let expr = {
+ // Push the current location on the stack
+ self.stack.push(location);
+ // Resolve the import recursively
+ // WARNING: do not propagate errors here or the stack will get messed up.
+ let result = do_resolve(self);
+ // Remove location from the stack.
+ location = self.stack.pop().unwrap();
+ result
+ }?;
// Add the resolved import to the cache
self.cache.insert(location, expr.clone());
diff --git a/dhall/src/semantics/resolve/hir.rs b/dhall/src/semantics/resolve/hir.rs
index 9256425..8869915 100644
--- a/dhall/src/semantics/resolve/hir.rs
+++ b/dhall/src/semantics/resolve/hir.rs
@@ -59,6 +59,10 @@ impl Hir {
let opts = ToExprOptions { alpha: false };
self.to_expr(opts)
}
+ pub fn to_expr_alpha(&self) -> Expr {
+ let opts = ToExprOptions { alpha: true };
+ self.to_expr(opts)
+ }
pub fn to_expr_tyenv(&self, env: &TyEnv) -> Expr {
let opts = ToExprOptions { alpha: false };
let mut env = env.as_nameenv().clone();
diff --git a/dhall/src/semantics/resolve/resolve.rs b/dhall/src/semantics/resolve/resolve.rs
index 7745e0b..6e50fa6 100644
--- a/dhall/src/semantics/resolve/resolve.rs
+++ b/dhall/src/semantics/resolve/resolve.rs
@@ -10,7 +10,7 @@ use crate::semantics::{mkerr, Hir, HirKind, ImportEnv, NameEnv, Type};
use crate::syntax;
use crate::syntax::map::DupTreeMap;
use crate::syntax::{
- BinOp, Builtin, Expr, ExprKind, FilePath, FilePrefix, ImportMode,
+ BinOp, Builtin, Expr, ExprKind, FilePath, FilePrefix, Hash, ImportMode,
ImportTarget, Span, UnspannedExpr, URL,
};
use crate::{Parsed, Resolved};
@@ -208,6 +208,7 @@ fn resolve_one_import(
env: &mut ImportEnv,
import: &Import,
location: &ImportLocation,
+ span: Span,
) -> Result<TypedHir, Error> {
let do_sanity_check = import.mode != ImportMode::Location;
let location = location.chain(&import.location, do_sanity_check)?;
@@ -215,7 +216,30 @@ fn resolve_one_import(
ImportMode::Code => {
let parsed = location.fetch_dhall()?;
let typed = resolve_with_env(env, parsed)?.typecheck()?;
- Ok((typed.normalize().to_hir(), typed.ty().clone()))
+ let hir = typed.normalize().to_hir();
+ let ty = typed.ty().clone();
+ match &import.hash {
+ Some(Hash::SHA256(hash)) => {
+ let actual_hash = hir.to_expr_alpha().hash()?;
+ if hash[..] != actual_hash[..] {
+ mkerr(
+ ErrorBuilder::new("hash mismatch")
+ .span_err(span, "hash mismatch")
+ .note(format!(
+ "Expected sha256:{}",
+ hex::encode(hash)
+ ))
+ .note(format!(
+ "Found sha256:{}",
+ hex::encode(actual_hash)
+ ))
+ .format(),
+ )?
+ }
+ }
+ None => {}
+ }
+ Ok((hir, ty))
}
ImportMode::RawText => {
let text = location.fetch_text()?;
@@ -268,7 +292,7 @@ fn desugar(expr: &Expr) -> Cow<'_, Expr> {
fn traverse_resolve_expr(
name_env: &mut NameEnv,
expr: &Expr,
- f: &mut impl FnMut(Import) -> Result<TypedHir, Error>,
+ f: &mut impl FnMut(Import, Span) -> Result<TypedHir, Error>,
) -> Result<Hir, Error> {
let expr = desugar(expr);
Ok(match expr.kind() {
@@ -307,7 +331,7 @@ fn traverse_resolve_expr(
ExprKind::Import(import) => {
// TODO: evaluate import headers
let import = import.traverse_ref(|_| Ok::<_, Error>(()))?;
- let imported = f(import)?;
+ let imported = f(import, expr.span())?;
HirKind::Import(imported.0, imported.1)
}
kind => HirKind::Expr(kind),
@@ -322,10 +346,11 @@ fn resolve_with_env(
parsed: Parsed,
) -> Result<Resolved, Error> {
let Parsed(expr, location) = parsed;
- let resolved =
- traverse_resolve_expr(&mut NameEnv::new(), &expr, &mut |import| {
- resolve_one_import(env, &import, &location)
- })?;
+ let resolved = traverse_resolve_expr(
+ &mut NameEnv::new(),
+ &expr,
+ &mut |import, span| resolve_one_import(env, &import, &location, span),
+ )?;
Ok(Resolved(resolved))
}
@@ -334,7 +359,7 @@ pub fn resolve(parsed: Parsed) -> Result<Resolved, Error> {
}
pub fn skip_resolve_expr(expr: &Expr) -> Result<Hir, Error> {
- traverse_resolve_expr(&mut NameEnv::new(), expr, &mut |import| {
+ traverse_resolve_expr(&mut NameEnv::new(), expr, &mut |import, _span| {
Err(ImportError::UnexpectedImport(import).into())
})
}
diff --git a/dhall/src/syntax/ast/expr.rs b/dhall/src/syntax/ast/expr.rs
index 6ba6649..9e935dc 100644
--- a/dhall/src/syntax/ast/expr.rs
+++ b/dhall/src/syntax/ast/expr.rs
@@ -1,5 +1,6 @@
use std::collections::BTreeMap;
+use crate::error::Error;
use crate::semantics::Universe;
use crate::syntax::map::{DupTreeMap, DupTreeSet};
use crate::syntax::visitor;
@@ -255,6 +256,13 @@ impl Expr {
span,
}
}
+
+ // Compute the sha256 hash of the binary form of the expression.
+ pub fn hash(&self) -> Result<Box<[u8]>, Error> {
+ use sha2::Digest;
+ let data = binary::encode(self)?;
+ Ok(sha2::Sha256::digest(&data).as_slice().into())
+ }
}
// Empty enum to indicate that no error can occur
diff --git a/dhall/src/tests.rs b/dhall/src/tests.rs
index 2cd354f..5bcdb1c 100644
--- a/dhall/src/tests.rs
+++ b/dhall/src/tests.rs
@@ -63,6 +63,7 @@ enum Test {
BinaryDecodingFailure(TestFile, TestFile),
ImportSuccess(TestFile, TestFile),
ImportFailure(TestFile, TestFile),
+ SemanticHash(TestFile, TestFile),
TypeInferenceSuccess(TestFile, TestFile),
TypeInferenceFailure(TestFile, TestFile),
Normalization(TestFile, TestFile),
@@ -132,7 +133,7 @@ impl TestFile {
fn write_ui(&self, x: impl Display) -> Result<()> {
match self {
TestFile::UI(_) => {}
- _ => panic!("Can't write an error to a non-UI file"),
+ _ => panic!("Can't write a ui string to a dhall file"),
}
let path = self.path();
create_dir_all(path.parent().unwrap())?;
@@ -302,6 +303,11 @@ fn run_test(test: Test) -> Result<()> {
let err = expr.resolve().unwrap_err();
expected.compare_ui(err)?;
}
+ SemanticHash(expr, expected) => {
+ let expr = expr.normalize()?.to_expr_alpha();
+ let hash = hex::encode(expr.hash()?);
+ expected.compare_ui(format!("sha256:{}", hash))?;
+ }
TypeInferenceSuccess(expr, expected) => {
let ty = expr.typecheck()?.get_type()?;
expected.compare(ty)?;
diff --git a/dhall/tests/import/failure/hashMismatch.txt b/dhall/tests/import/failure/hashMismatch.txt
new file mode 100644
index 0000000..2195959
--- /dev/null
+++ b/dhall/tests/import/failure/hashMismatch.txt
@@ -0,0 +1,8 @@
+Type error: error: hash mismatch
+ --> <current file>:1:1
+ |
+1 | ../data/simple.dhall sha256:aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa
+ | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ hash mismatch
+ |
+ = note: Expected sha256:aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa
+ = note: Found sha256:15f52ecf91c94c1baac02d5a4964b2ed8fa401641a2c8a95e8306ec7c1e3b8d2