diff options
| -rw-r--r-- | dhall/src/operations/typecheck.rs | 51 | ||||
| -rw-r--r-- | dhall/src/semantics/resolve/resolve.rs | 32 | ||||
| -rw-r--r-- | dhall/tests/spec.rs | 7 | ||||
| -rw-r--r-- | dhall/tests/type-inference/failure/unit/WithInvalidOverrideA.txt | 4 | ||||
| -rw-r--r-- | dhall/tests/type-inference/failure/unit/WithNotRecord.txt | 4 |
5 files changed, 57 insertions, 41 deletions
diff --git a/dhall/src/operations/typecheck.rs b/dhall/src/operations/typecheck.rs index 2ccc17d..af6f706 100644 --- a/dhall/src/operations/typecheck.rs +++ b/dhall/src/operations/typecheck.rs @@ -503,7 +503,56 @@ pub fn typecheck_operation( selection_val } - Completion(..) | With(..) => { + With(record, labels, expr) => { + use crate::syntax::Label; + use std::iter::{once, FromIterator}; + + let record_entries = |nk: &NirKind| { + match nk { + NirKind::RecordType(kts) => Ok(kts.clone()), + _ => mk_span_err(span.clone(), "WithMustBeRecord"), // TODO better error + } + }; + + let mut current_nk: Option<NirKind> = + Some(record.ty().kind().clone()); + let mut visited: Vec<(&Label, HashMap<Label, Nir>)> = Vec::new(); + let mut to_create = Vec::new(); + + for label in labels { + match current_nk { + None => to_create.push(label), + Some(nk) => { + let kts = record_entries(&nk)?; + + current_nk = + kts.get(label).map(|nir| nir.kind().clone()); + 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(FromIterator::from_iter(once(( + label.clone(), + nir, + )))); + 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); + } + + nir.to_type(Const::Type) + } + 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..c93be7e 100644 --- a/dhall/tests/spec.rs +++ b/dhall/tests/spec.rs @@ -544,12 +544,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 | |