From 85d946016d67515aa70fa01338512e3fd7df408e Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Mon, 2 Nov 2020 04:06:05 +0000 Subject: Typecheck `with` using mutation --- dhall/src/operations/typecheck.rs | 63 ++++++++++++------------------------ dhall/src/semantics/tck/tir.rs | 3 ++ dhall/src/semantics/tck/typecheck.rs | 4 +-- 3 files changed, 25 insertions(+), 45 deletions(-) diff --git a/dhall/src/operations/typecheck.rs b/dhall/src/operations/typecheck.rs index 9329aff..3016fea 100644 --- a/dhall/src/operations/typecheck.rs +++ b/dhall/src/operations/typecheck.rs @@ -48,8 +48,8 @@ fn typecheck_binop( env: &TyEnv, span: Span, op: BinOp, - l: &Tir<'_>, - r: &Tir<'_>, + l: Tir<'_>, + r: Tir<'_>, ) -> Result { let span_err = |msg: &str| mk_span_err(span.clone(), msg); use BinOp::*; @@ -290,7 +290,7 @@ fn typecheck_merge( pub fn typecheck_operation( env: &TyEnv, span: Span, - opkind: &OpKind>, + opkind: OpKind>, ) -> Result { let span_err = |msg: &str| mk_span_err(span.clone(), msg); use NirKind::{ListType, PiClosure, RecordType, UnionType}; @@ -345,7 +345,7 @@ pub fn typecheck_operation( ), } } - BinOp(o, l, r) => typecheck_binop(env, span, *o, l, r)?, + BinOp(o, l, r) => typecheck_binop(env, span, o, l, r)?, BoolIf(x, y, z) => { if *x.ty().kind() != NirKind::from_builtin(Builtin::Bool) { return span_err("InvalidPredicate"); @@ -360,7 +360,7 @@ pub fn typecheck_operation( y.ty().clone() } Merge(record, scrut, type_annot) => { - typecheck_merge(env, span, record, scrut, type_annot.as_ref())? + typecheck_merge(env, span, &record, &scrut, type_annot.as_ref())? } ToMap(record, annot) => { if record.ty().ty().as_const() != Some(Const::Type) { @@ -434,14 +434,14 @@ pub fn typecheck_operation( } Field(scrut, x) => { match scrut.ty().kind() { - RecordType(kts) => match kts.get(x) { + RecordType(kts) => match kts.get(&x) { Some(val) => Type::new_infer_universe(env, val.clone())?, None => return span_err("MissingRecordField"), }, NirKind::Const(_) => { let scrut = scrut.eval_to_type(env)?; match scrut.kind() { - UnionType(kts) => match kts.get(x) { + UnionType(kts) => match kts.get(&x) { // Constructor has type T -> < x: T, ... > Some(Some(ty)) => Nir::from_kind(PiClosure { binder: Binder::new(x.clone()), @@ -467,7 +467,7 @@ pub fn typecheck_operation( let mut new_kts = HashMap::new(); for l in labels { - match kts.get(l) { + match kts.get(&l) { None => return span_err("ProjectionMissingEntry"), Some(t) => { new_kts.insert(l.clone(), t.clone()); @@ -504,45 +504,22 @@ pub fn typecheck_operation( selection_val } With(record, labels, expr) => { - use crate::syntax::Label; - use std::iter::once; - - let mut current_nir: Option = - Some(record.ty().as_nir().clone()); - let mut visited: Vec<(&Label, HashMap)> = Vec::new(); - let mut to_create = Vec::new(); - + let mut record_ty = record.into_ty().into_nir(); + let mut current = &mut record_ty; + // We dig through the current record type with the provided labels. 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)); - } + if let RecordType(kts) = current.kind_mut() { + // Get existing entry or insert empty record type into it. + current = kts.entry(label).or_insert_with(|| { + Nir::from_kind(RecordType(HashMap::new())) + }); + } else { + return mk_span_err(span.clone(), "WithMustBeRecord"); } } + *current = expr.into_ty().into_nir(); - // 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)? + Type::new_infer_universe(env, record_ty)? } Completion(..) => { unreachable!("This case should have been handled in resolution") diff --git a/dhall/src/semantics/tck/tir.rs b/dhall/src/semantics/tck/tir.rs index ec15a1f..f34802c 100644 --- a/dhall/src/semantics/tck/tir.rs +++ b/dhall/src/semantics/tck/tir.rs @@ -117,6 +117,9 @@ impl<'hir> Tir<'hir> { pub fn ty(&self) -> &Type { &self.ty } + pub fn into_ty(self) -> Type { + self.ty + } pub fn to_hir(&self) -> Hir { self.as_hir().clone() diff --git a/dhall/src/semantics/tck/typecheck.rs b/dhall/src/semantics/tck/typecheck.rs index d21c7ce..498bd76 100644 --- a/dhall/src/semantics/tck/typecheck.rs +++ b/dhall/src/semantics/tck/typecheck.rs @@ -35,7 +35,7 @@ fn type_one_layer( ) -> Result { let span_err = |msg: &str| mk_span_err(span.clone(), msg); - Ok(match &ekind { + Ok(match ekind { ExprKind::Import(..) => { unreachable!("This case should have been handled in resolution") } @@ -57,7 +57,7 @@ fn type_one_layer( NumKind::Double(_) => Builtin::Double, }), ExprKind::Builtin(b) => { - let t_hir = type_of_builtin(*b); + let t_hir = type_of_builtin(b); typecheck(&t_hir)?.eval_to_type(env)? } ExprKind::TextLit(interpolated) => { -- cgit v1.2.3