diff options
author | Nadrieril | 2020-11-02 23:00:00 +0000 |
---|---|---|
committer | GitHub | 2020-11-02 23:00:00 +0000 |
commit | 6e4ad109e7b42eda68053c898dc7aa44199319bf (patch) | |
tree | 30c37039b161e7ce913e5fb41ff4a30bc6d7e622 /dhall/src | |
parent | 2839bfe23b7a0916e9e625a4d62835c39d8693ba (diff) | |
parent | 527b05b66d84c6acaef904f7143a87a1eff67858 (diff) |
Merge pull request #193 from basile-henry/with-no-desugar
Diffstat (limited to '')
-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 |
3 files changed, 103 insertions, 33 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), } } |