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/normalization.rs') 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/normalization.rs') 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 ++++++++++--------------- 1 file changed, 10 insertions(+), 15 deletions(-) (limited to 'dhall/src/operations/normalization.rs') 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); } } -- cgit v1.2.3