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') 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 aaac028d21b02827a0c79b34728fb104e5649149 Mon Sep 17 00:00:00 2001 From: Basile Henry Date: Sun, 1 Nov 2020 23:14:12 +0100 Subject: Implement normalization for With op --- dhall/src/operations/normalization.rs | 45 +++++++++++++++++++++++++++++++++-- 1 file changed, 43 insertions(+), 2 deletions(-) (limited to 'dhall/src/operations') diff --git a/dhall/src/operations/normalization.rs b/dhall/src/operations/normalization.rs index b930f93..908ed93 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,48 @@ pub fn normalize_operation(opkind: &OpKind) -> Ret { )), _ => nothing_to_do(), }, - Completion(..) | With(..) => { + With(record, labels, expr) => { + use std::iter::FromIterator; + + let mut current_nk: Option = Some(record.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) => match nk { + RecordLit(kvs) => { + current_nk = + kvs.get(label).map(|nir| nir.kind().clone()); + visited.push((label, kvs)); + } + _ => return nothing_to_do(), + }, + } + } + + // Create Nir for record bottom up + let mut nir = expr.clone(); + + while let Some(label) = to_create.pop() { + let rec = RecordLit(FromIterator::from_iter(once(( + label.clone(), + nir, + )))); + nir = Nir::from_kind(rec); + } + + // 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") } } -- cgit v1.2.3 From 7066e625fc945e66d8af91c633e762fe5f7b17f5 Mon Sep 17 00:00:00 2001 From: Basile Henry Date: Sun, 1 Nov 2020 23:33:38 +0100 Subject: Handle partially abstract with --- dhall/src/operations/normalization.rs | 37 +++++++++++++++++++++++++++-------- 1 file changed, 29 insertions(+), 8 deletions(-) (limited to 'dhall/src/operations') diff --git a/dhall/src/operations/normalization.rs b/dhall/src/operations/normalization.rs index 908ed93..f147f85 100644 --- a/dhall/src/operations/normalization.rs +++ b/dhall/src/operations/normalization.rs @@ -306,16 +306,24 @@ pub fn normalize_operation(opkind: &OpKind) -> Ret { let mut visited: Vec<(&Label, HashMap)> = 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_nk { - None => to_create.push(label), + None => to_create.push(label.clone()), Some(nk) => match nk { RecordLit(kvs) => { current_nk = kvs.get(label).map(|nir| nir.kind().clone()); visited.push((label, kvs)); } - _ => return nothing_to_do(), + // Handle partially abstract case + nir => { + abstract_nir = Some(Nir::from_kind(nir)); + to_create.push(label.clone()); + current_nk = None; + } }, } } @@ -323,12 +331,25 @@ pub fn normalize_operation(opkind: &OpKind) -> Ret { // Create Nir for record bottom up let mut nir = expr.clone(); - while let Some(label) = to_create.pop() { - let rec = RecordLit(FromIterator::from_iter(once(( - label.clone(), - nir, - )))); - nir = Nir::from_kind(rec); + match abstract_nir { + // No abstract nir, creating singleton records + None => { + while let Some(label) = to_create.pop() { + let rec = RecordLit(FromIterator::from_iter(once(( + label.clone(), + nir, + )))); + 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 -- 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/normalization.rs | 25 ++++++++++--------------- dhall/src/operations/typecheck.rs | 24 ++++++++++-------------- 2 files changed, 20 insertions(+), 29 deletions(-) (limited to 'dhall/src/operations') diff --git a/dhall/src/operations/normalization.rs b/dhall/src/operations/normalization.rs index f147f85..dbd58f9 100644 --- a/dhall/src/operations/normalization.rs +++ b/dhall/src/operations/normalization.rs @@ -300,9 +300,7 @@ pub fn normalize_operation(opkind: &OpKind) -> Ret { _ => nothing_to_do(), }, With(record, labels, expr) => { - use std::iter::FromIterator; - - let mut current_nk: Option = Some(record.kind().clone()); + let mut current_nir: Option = Some(record.clone()); let mut visited: Vec<(&Label, HashMap)> = Vec::new(); let mut to_create = Vec::new(); @@ -310,19 +308,18 @@ pub fn normalize_operation(opkind: &OpKind) -> Ret { let mut abstract_nir = None; for label in labels { - match current_nk { + match current_nir { None => to_create.push(label.clone()), - Some(nk) => match nk { + Some(nir) => match nir.kind() { RecordLit(kvs) => { - current_nk = - kvs.get(label).map(|nir| nir.kind().clone()); - visited.push((label, kvs)); + current_nir = kvs.get(label).cloned(); + visited.push((label, kvs.clone())); } // Handle partially abstract case - nir => { - abstract_nir = Some(Nir::from_kind(nir)); + _ => { + abstract_nir = Some(nir); to_create.push(label.clone()); - current_nk = None; + current_nir = None; } }, } @@ -335,10 +332,8 @@ pub fn normalize_operation(opkind: &OpKind) -> Ret { // No abstract nir, creating singleton records None => { while let Some(label) = to_create.pop() { - let rec = RecordLit(FromIterator::from_iter(once(( - label.clone(), - nir, - )))); + let rec = + RecordLit(once((label.clone(), nir)).collect()); nir = Nir::from_kind(rec); } } 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') 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') 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