summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorNadrieril2020-11-02 23:00:00 +0000
committerGitHub2020-11-02 23:00:00 +0000
commit6e4ad109e7b42eda68053c898dc7aa44199319bf (patch)
tree30c37039b161e7ce913e5fb41ff4a30bc6d7e622
parent2839bfe23b7a0916e9e625a4d62835c39d8693ba (diff)
parent527b05b66d84c6acaef904f7143a87a1eff67858 (diff)
Merge pull request #193 from basile-henry/with-no-desugar
Diffstat (limited to '')
-rw-r--r--dhall/src/operations/normalization.rs61
-rw-r--r--dhall/src/operations/typecheck.rs43
-rw-r--r--dhall/src/semantics/resolve/resolve.rs32
-rw-r--r--dhall/tests/spec.rs11
-rw-r--r--dhall/tests/type-inference/failure/unit/WithInvalidOverrideA.txt4
-rw-r--r--dhall/tests/type-inference/failure/unit/WithNotRecord.txt4
6 files changed, 108 insertions, 47 deletions
diff --git a/dhall/src/operations/normalization.rs b/dhall/src/operations/normalization.rs
index b930f93..dbd58f9 100644
--- a/dhall/src/operations/normalization.rs
+++ b/dhall/src/operations/normalization.rs
@@ -4,7 +4,7 @@ use std::iter::once;
use crate::operations::{BinOp, OpKind};
use crate::semantics::{
- merge_maps, ret_kind, ret_op, ret_ref, Nir, NirKind, Ret, TextLit,
+ merge_maps, ret_kind, ret_nir, ret_op, ret_ref, Nir, NirKind, Ret, TextLit,
};
use crate::syntax::{ExprKind, Label, NumKind};
@@ -299,7 +299,64 @@ pub fn normalize_operation(opkind: &OpKind<Nir>) -> Ret {
)),
_ => nothing_to_do(),
},
- Completion(..) | With(..) => {
+ With(record, labels, expr) => {
+ let mut current_nir: Option<Nir> = Some(record.clone());
+ let mut visited: Vec<(&Label, HashMap<Label, Nir>)> = Vec::new();
+ let mut to_create = Vec::new();
+
+ // To be used when an abstract entry is reached
+ let mut abstract_nir = None;
+
+ for label in labels {
+ match current_nir {
+ None => to_create.push(label.clone()),
+ Some(nir) => match nir.kind() {
+ RecordLit(kvs) => {
+ current_nir = kvs.get(label).cloned();
+ visited.push((label, kvs.clone()));
+ }
+ // Handle partially abstract case
+ _ => {
+ abstract_nir = Some(nir);
+ to_create.push(label.clone());
+ current_nir = None;
+ }
+ },
+ }
+ }
+
+ // Create Nir for record bottom up
+ let mut nir = expr.clone();
+
+ match abstract_nir {
+ // No abstract nir, creating singleton records
+ None => {
+ while let Some(label) = to_create.pop() {
+ let rec =
+ RecordLit(once((label.clone(), nir)).collect());
+ nir = Nir::from_kind(rec);
+ }
+ }
+ // Abstract nir, creating with op
+ Some(abstract_nir) => {
+ nir = Nir::from_kind(Op(OpKind::With(
+ abstract_nir,
+ to_create,
+ nir,
+ )));
+ }
+ }
+
+ // Update visited records
+ while let Some((label, mut kvs)) = visited.pop() {
+ kvs.insert(label.clone(), nir);
+ let rec = RecordLit(kvs);
+ nir = Nir::from_kind(rec);
+ }
+
+ ret_nir(nir)
+ }
+ Completion(..) => {
unreachable!("This case should have been handled in resolution")
}
}
diff --git a/dhall/src/operations/typecheck.rs b/dhall/src/operations/typecheck.rs
index 2ccc17d..9329aff 100644
--- a/dhall/src/operations/typecheck.rs
+++ b/dhall/src/operations/typecheck.rs
@@ -503,7 +503,48 @@ pub fn typecheck_operation(
selection_val
}
- Completion(..) | With(..) => {
+ With(record, labels, expr) => {
+ use crate::syntax::Label;
+ use std::iter::once;
+
+ let mut current_nir: Option<Nir> =
+ Some(record.ty().as_nir().clone());
+ let mut visited: Vec<(&Label, HashMap<Label, Nir>)> = Vec::new();
+ let mut to_create = Vec::new();
+
+ for label in labels {
+ match current_nir {
+ None => to_create.push(label),
+ Some(nir) => {
+ let kts = (match nir.kind() {
+ NirKind::RecordType(kts) => Ok(kts.clone()),
+ _ => mk_span_err(span.clone(), "WithMustBeRecord"), // TODO better error
+ })?;
+
+ current_nir = kts.get(label).cloned();
+ visited.push((label, kts));
+ }
+ }
+ }
+
+ // Create Nir for record type bottom up
+ let mut nir = expr.ty().as_nir().clone();
+
+ while let Some(label) = to_create.pop() {
+ let rec = RecordType(once((label.clone(), nir)).collect());
+ nir = Nir::from_kind(rec);
+ }
+
+ // Update visited records
+ while let Some((label, mut kts)) = visited.pop() {
+ kts.insert(label.clone(), nir);
+ let rec = RecordType(kts);
+ nir = Nir::from_kind(rec);
+ }
+
+ Type::new_infer_universe(env, nir)?
+ }
+ Completion(..) => {
unreachable!("This case should have been handled in resolution")
}
})
diff --git a/dhall/src/semantics/resolve/resolve.rs b/dhall/src/semantics/resolve/resolve.rs
index 572df25..dc1951e 100644
--- a/dhall/src/semantics/resolve/resolve.rs
+++ b/dhall/src/semantics/resolve/resolve.rs
@@ -2,7 +2,6 @@ use itertools::Itertools;
use std::borrow::Cow;
use std::collections::BTreeMap;
use std::env;
-use std::iter::once;
use std::path::PathBuf;
use url::Url;
@@ -13,8 +12,8 @@ use crate::operations::{BinOp, OpKind};
use crate::semantics::{mkerr, Hir, HirKind, ImportEnv, NameEnv, Type};
use crate::syntax;
use crate::syntax::{
- Expr, ExprKind, FilePath, FilePrefix, Hash, ImportMode, ImportTarget,
- Label, Span, UnspannedExpr, URL,
+ Expr, ExprKind, FilePath, FilePrefix, Hash, ImportMode, ImportTarget, Span,
+ UnspannedExpr, URL,
};
use crate::{Parsed, Resolved, Typed};
@@ -267,30 +266,6 @@ fn resolve_one_import(
Ok(Typed { hir, ty })
}
-/// Desugar a `with` expression.
-fn desugar_with(x: Expr, path: &[Label], y: Expr, span: Span) -> Expr {
- use crate::operations::BinOp::RightBiasedRecordMerge;
- use ExprKind::{Op, RecordLit};
- use OpKind::{BinOp, Field};
- let expr = |k| Expr::new(k, span.clone());
- match path {
- [] => y,
- [l, rest @ ..] => {
- let res = desugar_with(
- expr(Op(Field(x.clone(), l.clone()))),
- rest,
- y,
- span.clone(),
- );
- expr(Op(BinOp(
- RightBiasedRecordMerge,
- x,
- expr(RecordLit(once((l.clone(), res)).collect())),
- )))
- }
- }
-}
-
/// Desugar the first level of the expression.
fn desugar(expr: &Expr) -> Cow<'_, Expr> {
match expr.kind() {
@@ -316,9 +291,6 @@ fn desugar(expr: &Expr) -> Cow<'_, Expr> {
expr.span(),
))
}
- ExprKind::Op(OpKind::With(x, path, y)) => {
- Cow::Owned(desugar_with(x.clone(), path, y.clone(), expr.span()))
- }
_ => Cow::Borrowed(expr),
}
}
diff --git a/dhall/tests/spec.rs b/dhall/tests/spec.rs
index 36cbd81..357181a 100644
--- a/dhall/tests/spec.rs
+++ b/dhall/tests/spec.rs
@@ -521,10 +521,6 @@ fn define_features() -> Vec<TestFeature> {
|| path == "simple/integerToDouble"
// TODO: fix Double/show
|| path == "prelude/JSON/number/1"
- // With builtin not implemented yet
- || path == "unit/WithCreateIntermediateRecords"
- || path == "unit/WithDesugar"
- || path == "unit/WithPartiallyAbstract"
}),
..default_feature.clone()
},
@@ -544,12 +540,7 @@ fn define_features() -> Vec<TestFeature> {
variant: SpecTestKind::TypeInferenceSuccess,
// TODO: this fails because of caching shenanigans
// too_slow_path: Rc::new(|path: &str| path == "prelude"),
- exclude_path: Rc::new(|path: &str| {
- false
- || path == "prelude"
- // With builtin not implemented yet
- || path == "unit/WithCreateIntermediateRecords"
- }),
+ exclude_path: Rc::new(|path: &str| path == "prelude"),
..default_feature.clone()
},
TestFeature {
diff --git a/dhall/tests/type-inference/failure/unit/WithInvalidOverrideA.txt b/dhall/tests/type-inference/failure/unit/WithInvalidOverrideA.txt
index c34175f..c2af394 100644
--- a/dhall/tests/type-inference/failure/unit/WithInvalidOverrideA.txt
+++ b/dhall/tests/type-inference/failure/unit/WithInvalidOverrideA.txt
@@ -1,7 +1,7 @@
-Type error: error: MustCombineRecord
+Type error: error: WithMustBeRecord
--> <current file>:1:1
|
...
6 | { a = 1 } with a.b = 2
- | ^^^^^^^^^^^^^^^^^^^^^^ MustCombineRecord
+ | ^^^^^^^^^^^^^^^^^^^^^^ WithMustBeRecord
|
diff --git a/dhall/tests/type-inference/failure/unit/WithNotRecord.txt b/dhall/tests/type-inference/failure/unit/WithNotRecord.txt
index 8574e48..cd76485 100644
--- a/dhall/tests/type-inference/failure/unit/WithNotRecord.txt
+++ b/dhall/tests/type-inference/failure/unit/WithNotRecord.txt
@@ -1,6 +1,6 @@
-Type error: error: MustCombineRecord
+Type error: error: WithMustBeRecord
--> <current file>:1:1
|
1 | 5 with a = 10
- | ^^^^^^^^^^^^^ MustCombineRecord
+ | ^^^^^^^^^^^^^ WithMustBeRecord
|