diff options
| -rw-r--r-- | dhall/src/operations/normalization.rs | 61 | ||||
| -rw-r--r-- | dhall/src/operations/typecheck.rs | 43 | ||||
| -rw-r--r-- | dhall/src/semantics/resolve/resolve.rs | 32 | ||||
| -rw-r--r-- | dhall/tests/spec.rs | 11 | ||||
| -rw-r--r-- | dhall/tests/type-inference/failure/unit/WithInvalidOverrideA.txt | 4 | ||||
| -rw-r--r-- | dhall/tests/type-inference/failure/unit/WithNotRecord.txt | 4 |
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 | |