summaryrefslogtreecommitdiff
path: root/dhall/src/operations
diff options
context:
space:
mode:
authorNadrieril2020-09-15 00:10:48 +0100
committerGitHub2020-09-15 00:10:48 +0100
commit12752fb0ff108fcbc37f209384eb3d2720809fb7 (patch)
treeb7aa0f75932426461234e4b7568a6681247482ff /dhall/src/operations
parent97a3719a3b4fa88873cd128fb193444c5d4bb387 (diff)
parentd1ac40eea5d1e62762c4a20ba9d2dc5ed0d5e06e (diff)
Merge pull request #176 from Nadrieril/catchup-spec
Diffstat (limited to 'dhall/src/operations')
-rw-r--r--dhall/src/operations/kind.rs3
-rw-r--r--dhall/src/operations/normalization.rs2
-rw-r--r--dhall/src/operations/typecheck.rs2
3 files changed, 5 insertions, 2 deletions
diff --git a/dhall/src/operations/kind.rs b/dhall/src/operations/kind.rs
index 0ee9671..2b035ef 100644
--- a/dhall/src/operations/kind.rs
+++ b/dhall/src/operations/kind.rs
@@ -55,6 +55,8 @@ pub enum OpKind<SubExpr> {
ProjectionByExpr(SubExpr, SubExpr),
/// `x::y`
Completion(SubExpr, SubExpr),
+ /// `x with a.b.c = y`
+ With(SubExpr, Vec<Label>, SubExpr),
}
impl<SE> OpKind<SE> {
@@ -85,6 +87,7 @@ impl<SE> OpKind<SE> {
Projection(e, ls) => Projection(expr!(e), ls.clone()),
ProjectionByExpr(e, x) => ProjectionByExpr(expr!(e), expr!(x)),
Completion(e, x) => Completion(expr!(e), expr!(x)),
+ With(x, ls, y) => With(expr!(x), ls.clone(), expr!(y)),
})
}
diff --git a/dhall/src/operations/normalization.rs b/dhall/src/operations/normalization.rs
index 86fed13..b930f93 100644
--- a/dhall/src/operations/normalization.rs
+++ b/dhall/src/operations/normalization.rs
@@ -299,7 +299,7 @@ pub fn normalize_operation(opkind: &OpKind<Nir>) -> Ret {
)),
_ => nothing_to_do(),
},
- Completion(..) => {
+ Completion(..) | With(..) => {
unreachable!("This case should have been handled in resolution")
}
}
diff --git a/dhall/src/operations/typecheck.rs b/dhall/src/operations/typecheck.rs
index 314c587..2ccc17d 100644
--- a/dhall/src/operations/typecheck.rs
+++ b/dhall/src/operations/typecheck.rs
@@ -503,7 +503,7 @@ pub fn typecheck_operation(
selection_val
}
- Completion(..) => {
+ Completion(..) | With(..) => {
unreachable!("This case should have been handled in resolution")
}
})