summaryrefslogtreecommitdiff
path: root/dhall
diff options
context:
space:
mode:
Diffstat (limited to 'dhall')
-rw-r--r--dhall/src/phase/binary.rs16
-rw-r--r--dhall/src/phase/resolve.rs94
-rw-r--r--dhall/src/phase/typecheck.rs8
3 files changed, 65 insertions, 53 deletions
diff --git a/dhall/src/phase/binary.rs b/dhall/src/phase/binary.rs
index 4831c7e..8c98f77 100644
--- a/dhall/src/phase/binary.rs
+++ b/dhall/src/phase/binary.rs
@@ -5,8 +5,8 @@ use std::vec;
use dhall_syntax::map::DupTreeMap;
use dhall_syntax::{
- rc, Expr, ExprF, FilePrefix, Hash, Import, ImportLocation, ImportMode,
- Integer, InterpolatedText, Label, Natural, Scheme, URL, V, FilePath
+ rc, Expr, ExprF, FilePath, FilePrefix, Hash, Import, ImportLocation,
+ ImportMode, Integer, InterpolatedText, Label, Natural, Scheme, URL, V,
};
use crate::error::{DecodeError, EncodeError};
@@ -483,9 +483,13 @@ where
BoolIf(x, y, z) => ser_seq!(ser; tag(14), expr(x), expr(y), expr(z)),
Var(V(l, n)) if l == &"_".into() => ser.serialize_u64(*n as u64),
Var(V(l, n)) => ser_seq!(ser; label(l), U64(*n as u64)),
- Lam(l, x, y) if l == &"_".into() => ser_seq!(ser; tag(1), expr(x), expr(y)),
+ Lam(l, x, y) if l == &"_".into() => {
+ ser_seq!(ser; tag(1), expr(x), expr(y))
+ }
Lam(l, x, y) => ser_seq!(ser; tag(1), label(l), expr(x), expr(y)),
- Pi(l, x, y) if l == &"_".into() => ser_seq!(ser; tag(2), expr(x), expr(y)),
+ Pi(l, x, y) if l == &"_".into() => {
+ ser_seq!(ser; tag(2), expr(x), expr(y))
+ }
Pi(l, x, y) => ser_seq!(ser; tag(2), label(l), expr(x), expr(y)),
Let(_, _, _, _) => {
let (bound_e, bindings) = collect_nested_lets(e);
@@ -557,7 +561,9 @@ where
ser_seq!(ser; tag(3), U64(op), expr(x), expr(y))
}
Merge(x, y, None) => ser_seq!(ser; tag(6), expr(x), expr(y)),
- Merge(x, y, Some(z)) => ser_seq!(ser; tag(6), expr(x), expr(y), expr(z)),
+ Merge(x, y, Some(z)) => {
+ ser_seq!(ser; tag(6), expr(x), expr(y), expr(z))
+ }
ToMap(x, None) => ser_seq!(ser; tag(27), expr(x)),
ToMap(x, Some(y)) => ser_seq!(ser; tag(27), expr(x), expr(y)),
Projection(x, ls) => ser.collect_seq(
diff --git a/dhall/src/phase/resolve.rs b/dhall/src/phase/resolve.rs
index cccc7a7..c5f2ac8 100644
--- a/dhall/src/phase/resolve.rs
+++ b/dhall/src/phase/resolve.rs
@@ -38,9 +38,9 @@ fn resolve_import(
Here => cwd.join(path_buf),
_ => unimplemented!("{:?}", import),
};
- Ok(load_import(&path_buf, import_cache, import_stack).map_err(|e| {
- ImportError::Recursive(import.clone(), Box::new(e))
- })?)
+ Ok(load_import(&path_buf, import_cache, import_stack).map_err(
+ |e| ImportError::Recursive(import.clone(), Box::new(e)),
+ )?)
}
_ => unimplemented!("{:?}", import),
}
@@ -118,58 +118,60 @@ impl Canonicalize for FilePath {
let mut file_path_components = self.file_path.clone().into_iter();
loop {
- let component = file_path_components.next();
- match component.as_ref() {
- // ───────────────────
- // canonicalize(ε) = ε
- None => break,
-
- // canonicalize(directory₀) = directory₁
- // ───────────────────────────────────────
- // canonicalize(directory₀/.) = directory₁
- Some(c) if c == "." => continue,
-
- Some(c) if c == ".." => match file_path_components.next() {
- // canonicalize(directory₀) = ε
- // ────────────────────────────
- // canonicalize(directory₀/..) = /..
- None => file_path.push("..".to_string()),
-
- // canonicalize(directory₀) = directory₁/..
- // ──────────────────────────────────────────────
- // canonicalize(directory₀/..) = directory₁/../..
- Some(ref c) if c == ".." => {
- file_path.push("..".to_string());
- file_path.push("..".to_string());
- },
-
- // canonicalize(directory₀) = directory₁/component
- // ─────────────────────────────────────────────── ; If "component" is not
- // canonicalize(directory₀/..) = directory₁ ; ".."
- Some(_) => continue,
- },
-
- // canonicalize(directory₀) = directory₁
- // ───────────────────────────────────────────────────────── ; If no other
- // canonicalize(directory₀/component) = directory₁/component ; rule matches
- Some(c) => file_path.push(c.clone()),
- }
+ let component = file_path_components.next();
+ match component.as_ref() {
+ // ───────────────────
+ // canonicalize(ε) = ε
+ None => break,
+
+ // canonicalize(directory₀) = directory₁
+ // ───────────────────────────────────────
+ // canonicalize(directory₀/.) = directory₁
+ Some(c) if c == "." => continue,
+
+ Some(c) if c == ".." => match file_path_components.next() {
+ // canonicalize(directory₀) = ε
+ // ────────────────────────────
+ // canonicalize(directory₀/..) = /..
+ None => file_path.push("..".to_string()),
+
+ // canonicalize(directory₀) = directory₁/..
+ // ──────────────────────────────────────────────
+ // canonicalize(directory₀/..) = directory₁/../..
+ Some(ref c) if c == ".." => {
+ file_path.push("..".to_string());
+ file_path.push("..".to_string());
+ }
+
+ // canonicalize(directory₀) = directory₁/component
+ // ─────────────────────────────────────────────── ; If "component" is not
+ // canonicalize(directory₀/..) = directory₁ ; ".."
+ Some(_) => continue,
+ },
+
+ // canonicalize(directory₀) = directory₁
+ // ───────────────────────────────────────────────────────── ; If no other
+ // canonicalize(directory₀/component) = directory₁/component ; rule matches
+ Some(c) => file_path.push(c.clone()),
+ }
}
FilePath { file_path }
}
}
-impl<SE: Copy> Canonicalize for ImportLocation<SE> {
+impl<SE: Copy> Canonicalize for ImportLocation<SE> {
fn canonicalize(&self) -> ImportLocation<SE> {
match self {
- ImportLocation::Local(prefix, file) => ImportLocation::Local(*prefix, file.canonicalize()),
+ ImportLocation::Local(prefix, file) => {
+ ImportLocation::Local(*prefix, file.canonicalize())
+ }
ImportLocation::Remote(url) => ImportLocation::Remote(URL {
- scheme: url.scheme,
- authority: url.authority.clone(),
- path: url.path.canonicalize(),
- query: url.query.clone(),
- headers: url.headers.clone(),
+ scheme: url.scheme,
+ authority: url.authority.clone(),
+ path: url.path.canonicalize(),
+ query: url.query.clone(),
+ headers: url.headers.clone(),
}),
ImportLocation::Env(name) => ImportLocation::Env(name.to_string()),
ImportLocation::Missing => ImportLocation::Missing,
diff --git a/dhall/src/phase/typecheck.rs b/dhall/src/phase/typecheck.rs
index 2e61fbc..9013c1f 100644
--- a/dhall/src/phase/typecheck.rs
+++ b/dhall/src/phase/typecheck.rs
@@ -249,7 +249,9 @@ fn type_of_builtin<E>(b: Builtin) -> Expr<E> {
list
),
ListLength => make_type!(forall (a: Type) -> (List a) -> Natural),
- ListHead | ListLast => make_type!(forall (a: Type) -> (List a) -> Optional a),
+ ListHead | ListLast => {
+ make_type!(forall (a: Type) -> (List a) -> Optional a)
+ }
ListIndexed => make_type!(
forall (a: Type) ->
(List a) ->
@@ -373,7 +375,9 @@ fn type_last_layer(
Import(_) => unreachable!(
"There should remain no imports in a resolved expression"
),
- Lam(_, _, _) | Pi(_, _, _) | Let(_, _, _, _) | Embed(_) | Var(_) => unreachable!(),
+ Lam(_, _, _) | Pi(_, _, _) | Let(_, _, _, _) | Embed(_) | Var(_) => {
+ unreachable!()
+ }
App(f, a) => {
let tf = f.get_type()?;
let tf_borrow = tf.as_whnf();
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-23 16:06:50 +0000