From 6987b275e4bf5f545d823d186ce08a2fe9a3eb44 Mon Sep 17 00:00:00 2001 From: Basile Henry Date: Sun, 1 Nov 2020 22:46:35 +0100 Subject: Implement type checking for With op --- dhall/src/operations/typecheck.rs | 51 ++++++++++++++++++++++++++++++++++++++- 1 file changed, 50 insertions(+), 1 deletion(-) (limited to 'dhall/src/operations/typecheck.rs') 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 = + Some(record.ty().kind().clone()); + let mut visited: Vec<(&Label, HashMap)> = 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") } }) -- cgit v1.2.3 From f485ad425a786b680526a36a23bf58db9b0224e4 Mon Sep 17 00:00:00 2001 From: Basile Henry Date: Mon, 2 Nov 2020 23:06:29 +0100 Subject: Refactor following PR review --- dhall/src/operations/typecheck.rs | 24 ++++++++++-------------- 1 file changed, 10 insertions(+), 14 deletions(-) (limited to 'dhall/src/operations/typecheck.rs') diff --git a/dhall/src/operations/typecheck.rs b/dhall/src/operations/typecheck.rs index af6f706..6da7027 100644 --- a/dhall/src/operations/typecheck.rs +++ b/dhall/src/operations/typecheck.rs @@ -505,28 +505,27 @@ pub fn typecheck_operation( } With(record, labels, expr) => { use crate::syntax::Label; - use std::iter::{once, FromIterator}; + use std::iter::once; - let record_entries = |nk: &NirKind| { - match nk { + let record_entries = |nir: &Nir| { + match nir.kind() { NirKind::RecordType(kts) => Ok(kts.clone()), _ => mk_span_err(span.clone(), "WithMustBeRecord"), // TODO better error } }; - let mut current_nk: Option = - Some(record.ty().kind().clone()); + 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(); for label in labels { - match current_nk { + match current_nir { None => to_create.push(label), - Some(nk) => { - let kts = record_entries(&nk)?; + Some(nir) => { + let kts = record_entries(&nir)?; - current_nk = - kts.get(label).map(|nir| nir.kind().clone()); + current_nir = kts.get(label).cloned(); visited.push((label, kts)); } } @@ -536,10 +535,7 @@ pub fn typecheck_operation( 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, - )))); + let rec = RecordType(once((label.clone(), nir)).collect()); nir = Nir::from_kind(rec); } -- cgit v1.2.3 From 8b016bbabb6be73f395feda73e4e40a4c552536b Mon Sep 17 00:00:00 2001 From: Basile Henry Date: Mon, 2 Nov 2020 23:09:14 +0100 Subject: Inline helper function --- dhall/src/operations/typecheck.rs | 12 ++++-------- 1 file changed, 4 insertions(+), 8 deletions(-) (limited to 'dhall/src/operations/typecheck.rs') diff --git a/dhall/src/operations/typecheck.rs b/dhall/src/operations/typecheck.rs index 6da7027..bab80dc 100644 --- a/dhall/src/operations/typecheck.rs +++ b/dhall/src/operations/typecheck.rs @@ -507,13 +507,6 @@ pub fn typecheck_operation( use crate::syntax::Label; use std::iter::once; - let record_entries = |nir: &Nir| { - match nir.kind() { - NirKind::RecordType(kts) => Ok(kts.clone()), - _ => mk_span_err(span.clone(), "WithMustBeRecord"), // TODO better error - } - }; - let mut current_nir: Option = Some(record.ty().as_nir().clone()); let mut visited: Vec<(&Label, HashMap)> = Vec::new(); @@ -523,7 +516,10 @@ pub fn typecheck_operation( match current_nir { None => to_create.push(label), Some(nir) => { - let kts = record_entries(&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)); -- cgit v1.2.3 From 6375a0f2c3b123af5b1ff8c79d02caef6d2ed7e1 Mon Sep 17 00:00:00 2001 From: Basile Henry Date: Mon, 2 Nov 2020 23:38:03 +0100 Subject: Handle record type properly --- dhall/src/operations/typecheck.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'dhall/src/operations/typecheck.rs') diff --git a/dhall/src/operations/typecheck.rs b/dhall/src/operations/typecheck.rs index bab80dc..9329aff 100644 --- a/dhall/src/operations/typecheck.rs +++ b/dhall/src/operations/typecheck.rs @@ -542,7 +542,7 @@ pub fn typecheck_operation( nir = Nir::from_kind(rec); } - nir.to_type(Const::Type) + Type::new_infer_universe(env, nir)? } Completion(..) => { unreachable!("This case should have been handled in resolution") -- cgit v1.2.3