From c4552a079aa5707188e1e9ad64cdf8cf646ade56 Mon Sep 17 00:00:00 2001 From: Eduardo Sandalo Porto Date: Fri, 5 Apr 2024 19:58:06 -0300 Subject: [PATCH 01/15] Start implementing automatic constructor generation --- src/book/mod.rs | 42 ++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 42 insertions(+) diff --git a/src/book/mod.rs b/src/book/mod.rs index 334ead7..83fcd54 100644 --- a/src/book/mod.rs +++ b/src/book/mod.rs @@ -2,6 +2,7 @@ use crate::{*}; use std::collections::BTreeMap; use std::collections::BTreeSet; +use std::iter::once; mod compile; mod parse; @@ -77,6 +78,47 @@ impl Book { def_term.get_free_vars(im::Vector::new(), &mut dependencies); for ref_name in dependencies { if let Err(_) = self.load(&base, &ref_name) { + // If `ref_name` is an unbound constructor of the ADT `def_term`, + // we can generate it. + + // TODO: returning None since the ADT is wrapped in an `Ann` term + println!("{:?}", def_term); + let maybe_ctrs = def_term.as_adt().map(|adt| adt.ctrs); + + let maybe_ref = maybe_ctrs.clone() + .and_then(|ctrs| ctrs.into_iter().find(|ctr| ctr.name == ref_name)); + + let maybe_names = maybe_ctrs + .map(|ctrs| ctrs.into_iter().map(|ctr| ctr.name)); + + // TODO: move this to the desugaring module once it is refactored + // TODO: test if it matches all of the implemented book + if let (Some(names), Some(ctr)) = (maybe_names, maybe_ref) { + let format_idx = |idx: &Term| format!("<{}>", idx.show()); + let format_fld = |(name, typ): &(String, Term)| format!("({name}: {})", typ.show()); + let format_ctr = |ctr_name| format!("λ{ctr_name}"); + + let ctr_text = once(ctr.name.clone()) + .chain(ctr.idxs.iter().map(format_idx)) + .chain(ctr.flds.iter().map(format_fld)) + .chain(once(":".to_string())) + .chain(once(def_term.format().flatten(None))) + .chain(once("=\n".to_string())) + .chain(once("~λP".to_string())) + .chain(names.map(format_ctr)) + .chain(once("(".to_string())) + .chain(once(ctr.name.clone())) + .chain(ctr.flds.iter().map(|(fld_name, _)| fld_name.clone())) + .chain(once(")".to_string())) + .collect::>() + .join(" "); + + println!("{}", ctr_text); + let ctr_code = KindParser::new(&ctr_text).parse_term(fid, &im::HashMap::new()); + + // continue; + } + self.handle_unbound(&file, &ref_name)?; } } From 3320fafe970791ddd55ee5ed8decf6bacc188b50 Mon Sep 17 00:00:00 2001 From: Eduardo Sandalo Porto Date: Sat, 6 Apr 2024 11:45:30 -0300 Subject: [PATCH 02/15] Correctly resugar ADT for constructor generation TODO: fix constructor name comparison --- src/book/mod.rs | 11 ++++++++--- 1 file changed, 8 insertions(+), 3 deletions(-) diff --git a/src/book/mod.rs b/src/book/mod.rs index 83fcd54..5fb3613 100644 --- a/src/book/mod.rs +++ b/src/book/mod.rs @@ -80,11 +80,16 @@ impl Book { if let Err(_) = self.load(&base, &ref_name) { // If `ref_name` is an unbound constructor of the ADT `def_term`, // we can generate it. + let maybe_adt = match &def_term { + Term::Ann { val, .. } => val.as_adt(), + Term::Slf { .. } => def_term.as_adt(), + _ => None + }; - // TODO: returning None since the ADT is wrapped in an `Ann` term - println!("{:?}", def_term); - let maybe_ctrs = def_term.as_adt().map(|adt| adt.ctrs); + // println!("{:?}", maybe_adt); + let maybe_ctrs = maybe_adt.map(|adt| adt.ctrs); + // TODO: "Test/constructor/" != "constructor" let maybe_ref = maybe_ctrs.clone() .and_then(|ctrs| ctrs.into_iter().find(|ctr| ctr.name == ref_name)); From f60bea55f7d0665d8a57e41d1b6b1834ac1b6c13 Mon Sep 17 00:00:00 2001 From: Eduardo Sandalo Porto Date: Sun, 7 Apr 2024 22:10:09 -0300 Subject: [PATCH 03/15] Generate full constructor code TODO: Add new constructor to book and create file TODO: Test for all of the `book` --- src/book/mod.rs | 50 ++++++------------------------------------------ src/sugar/mod.rs | 46 ++++++++++++++++++++++++++++++++++++++++++++ 2 files changed, 52 insertions(+), 44 deletions(-) diff --git a/src/book/mod.rs b/src/book/mod.rs index 5fb3613..c2b6be7 100644 --- a/src/book/mod.rs +++ b/src/book/mod.rs @@ -2,7 +2,6 @@ use crate::{*}; use std::collections::BTreeMap; use std::collections::BTreeSet; -use std::iter::once; mod compile; mod parse; @@ -73,56 +72,19 @@ impl Book { self.defs.insert(def_name.clone(), def_value.clone()); } // Finds dependencies and loads them - for (_, def_term) in defs.defs.into_iter() { + for (def_name, def_term) in defs.defs.into_iter() { let mut dependencies = BTreeSet::new(); def_term.get_free_vars(im::Vector::new(), &mut dependencies); for ref_name in dependencies { if let Err(_) = self.load(&base, &ref_name) { // If `ref_name` is an unbound constructor of the ADT `def_term`, // we can generate it. - let maybe_adt = match &def_term { - Term::Ann { val, .. } => val.as_adt(), - Term::Slf { .. } => def_term.as_adt(), - _ => None - }; - - // println!("{:?}", maybe_adt); - let maybe_ctrs = maybe_adt.map(|adt| adt.ctrs); - - // TODO: "Test/constructor/" != "constructor" - let maybe_ref = maybe_ctrs.clone() - .and_then(|ctrs| ctrs.into_iter().find(|ctr| ctr.name == ref_name)); - - let maybe_names = maybe_ctrs - .map(|ctrs| ctrs.into_iter().map(|ctr| ctr.name)); - - // TODO: move this to the desugaring module once it is refactored - // TODO: test if it matches all of the implemented book - if let (Some(names), Some(ctr)) = (maybe_names, maybe_ref) { - let format_idx = |idx: &Term| format!("<{}>", idx.show()); - let format_fld = |(name, typ): &(String, Term)| format!("({name}: {})", typ.show()); - let format_ctr = |ctr_name| format!("λ{ctr_name}"); - - let ctr_text = once(ctr.name.clone()) - .chain(ctr.idxs.iter().map(format_idx)) - .chain(ctr.flds.iter().map(format_fld)) - .chain(once(":".to_string())) - .chain(once(def_term.format().flatten(None))) - .chain(once("=\n".to_string())) - .chain(once("~λP".to_string())) - .chain(names.map(format_ctr)) - .chain(once("(".to_string())) - .chain(once(ctr.name.clone())) - .chain(ctr.flds.iter().map(|(fld_name, _)| fld_name.clone())) - .chain(once(")".to_string())) - .collect::>() - .join(" "); - - println!("{}", ctr_text); - let ctr_code = KindParser::new(&ctr_text).parse_term(fid, &im::HashMap::new()); - + let maybe_ctr_code = Term::constructor_code((&def_name, &def_term), &ref_name); + if let Some(ctr_code) = maybe_ctr_code { + // println!("got constructor!"); + // let ctr_code = KindParser::new(&ctr_text).parse_term(fid, &im::HashMap::new()); // continue; - } + } self.handle_unbound(&file, &ref_name)?; } diff --git a/src/sugar/mod.rs b/src/sugar/mod.rs index 941de0b..d5a0715 100644 --- a/src/sugar/mod.rs +++ b/src/sugar/mod.rs @@ -662,6 +662,52 @@ impl Term { return term; } + // TODO: test if it matches all of the implemented book + pub fn constructor_code((adt_name, adt_term): (&str, &Term), ctr_name: &str) -> Option { + let (adt, adt_typ) = match &adt_term { + // Type variables wrap ADTs in Lams + Term::Lam { bod, .. } => return Term::constructor_code((adt_name, bod), ctr_name), + // Skip `Ann` and `Src` + Term::Ann { val, .. } => return Term::constructor_code((adt_name, val), ctr_name), + Term::Src { val, .. } => return Term::constructor_code((adt_name, val), ctr_name), + // Found an ADT + Term::Slf { typ, .. } => (adt_term.as_adt()?, typ.show()), + _ => return None, + }; + + let ctrs = adt.ctrs.clone(); + let ctr_name = ctr_name.trim_end_matches('/'); // last "/" is not part of name + + // NOTE: "{ADT}/{constructor}" != "{constructor}" + let ctr = ctrs.iter().find(|ctr| format!("{adt_name}/{}", ctr.name) == ctr_name)?.clone(); + let names = ctrs.into_iter().map(|ctr| ctr.name); + + // TODO: what should I do with ctr.idxs? + // let format_idx = ... + let format_param = |param| format!("<{}>", param); + let format_fld = |(name, typ): &(String, Term)| format!("({name}: {})", typ.show()); + let format_ctr_name = |ctr_name| format!("λ{ctr_name}"); + + // Generate constructor function + use std::iter::once; + let ctr_text = once(ctr.name.clone()) + // `as_adt` reads type parameters in reverse + .chain(adt.pars.iter().map(format_param).rev()) + .chain(ctr.flds.iter().map(format_fld)) + .chain(once(":".to_string())) + .chain(once(adt_typ)) + .chain(once("=\n".to_string())) + .chain(once("~λP".to_string())) + .chain(names.map(format_ctr_name)) + .chain(once("(".to_string())) + .chain(once(ctr.name.clone())) + .chain(ctr.flds.iter().map(|(fld_name, _)| fld_name.clone())) + .chain(once(")".to_string())) + .collect::>() + .join(" "); + + Some(ctr_text) + } } impl ADT { From 1f25fb8a0995e6a8e29f72aff4e2aced0101c298 Mon Sep 17 00:00:00 2001 From: Eduardo Sandalo Porto Date: Mon, 8 Apr 2024 11:58:54 -0300 Subject: [PATCH 04/15] Save and load generated constructor TODO: Test with current `book` --- src/book/mod.rs | 14 +++++++++----- 1 file changed, 9 insertions(+), 5 deletions(-) diff --git a/src/book/mod.rs b/src/book/mod.rs index c2b6be7..a321d19 100644 --- a/src/book/mod.rs +++ b/src/book/mod.rs @@ -79,11 +79,15 @@ impl Book { if let Err(_) = self.load(&base, &ref_name) { // If `ref_name` is an unbound constructor of the ADT `def_term`, // we can generate it. - let maybe_ctr_code = Term::constructor_code((&def_name, &def_term), &ref_name); - if let Some(ctr_code) = maybe_ctr_code { - // println!("got constructor!"); - // let ctr_code = KindParser::new(&ctr_text).parse_term(fid, &im::HashMap::new()); - // continue; + let maybe_ctr = Term::constructor_code((&def_name, &def_term), &ref_name); + + if let Some(ctr_code) = maybe_ctr { + let file = format!("{}.kind2", ref_name.trim_end_matches('/')); + std::fs::write(&file, ctr_code) + .map_err(|_| format!("ERROR: could not create file for generated constructor {ref_name}"))?; + + self.load(&base, &ref_name)?; + continue; } self.handle_unbound(&file, &ref_name)?; From cbad45f15bd714cd119fece5bf60f8b05e62531c Mon Sep 17 00:00:00 2001 From: Eduardo Sandalo Porto Date: Mon, 8 Apr 2024 21:04:44 -0300 Subject: [PATCH 05/15] Make constructor generation code prettier --- src/sugar/mod.rs | 47 ++++++++++++++++++++++------------------------- 1 file changed, 22 insertions(+), 25 deletions(-) diff --git a/src/sugar/mod.rs b/src/sugar/mod.rs index d5a0715..87b65b3 100644 --- a/src/sugar/mod.rs +++ b/src/sugar/mod.rs @@ -663,48 +663,45 @@ impl Term { } // TODO: test if it matches all of the implemented book - pub fn constructor_code((adt_name, adt_term): (&str, &Term), ctr_name: &str) -> Option { + pub fn constructor_code((adt_name, adt_term): (&str, &Term), ctr_ref: &str) -> Option { + // Check if `adt_name` really is an ADT let (adt, adt_typ) = match &adt_term { // Type variables wrap ADTs in Lams - Term::Lam { bod, .. } => return Term::constructor_code((adt_name, bod), ctr_name), + Term::Lam { bod, .. } => return Term::constructor_code((adt_name, bod), ctr_ref), // Skip `Ann` and `Src` - Term::Ann { val, .. } => return Term::constructor_code((adt_name, val), ctr_name), - Term::Src { val, .. } => return Term::constructor_code((adt_name, val), ctr_name), + Term::Ann { val, .. } => return Term::constructor_code((adt_name, val), ctr_ref), + Term::Src { val, .. } => return Term::constructor_code((adt_name, val), ctr_ref), // Found an ADT Term::Slf { typ, .. } => (adt_term.as_adt()?, typ.show()), _ => return None, }; let ctrs = adt.ctrs.clone(); - let ctr_name = ctr_name.trim_end_matches('/'); // last "/" is not part of name - // NOTE: "{ADT}/{constructor}" != "{constructor}" - let ctr = ctrs.iter().find(|ctr| format!("{adt_name}/{}", ctr.name) == ctr_name)?.clone(); + // Search for constructor in ADT + let ctr_ref = ctr_ref.trim_end_matches('/'); // last "/" is not part of name + let ctr = ctrs.iter().find(|ctr| format!("{adt_name}/{}", ctr.name) == ctr_ref)?.clone(); + let ctr_name = ctr.name; let names = ctrs.into_iter().map(|ctr| ctr.name); + // Generate constructor code // TODO: what should I do with ctr.idxs? // let format_idx = ... + let format_param = |param| format!("<{}>", param); - let format_fld = |(name, typ): &(String, Term)| format!("({name}: {})", typ.show()); + let params = adt.pars.iter().map(format_param).rev().collect::>().join(" "); + + let format_field = |(name, typ): &(String, Term)| format!("({name}: {})", typ.show()); + let fields = ctr.flds.iter().map(format_field).collect::>().join(" "); + let format_ctr_name = |ctr_name| format!("λ{ctr_name}"); + let ctr_names = names.map(format_ctr_name).collect::>().join(" "); + + let field_names = ctr.flds.iter().map(|(name, _)| name.clone()).collect::>().join(" "); - // Generate constructor function - use std::iter::once; - let ctr_text = once(ctr.name.clone()) - // `as_adt` reads type parameters in reverse - .chain(adt.pars.iter().map(format_param).rev()) - .chain(ctr.flds.iter().map(format_fld)) - .chain(once(":".to_string())) - .chain(once(adt_typ)) - .chain(once("=\n".to_string())) - .chain(once("~λP".to_string())) - .chain(names.map(format_ctr_name)) - .chain(once("(".to_string())) - .chain(once(ctr.name.clone())) - .chain(ctr.flds.iter().map(|(fld_name, _)| fld_name.clone())) - .chain(once(")".to_string())) - .collect::>() - .join(" "); + let ctr_text = format!( + "{ctr_name} {params} {fields}: {adt_typ} =\n ~λP {ctr_names} ({ctr_name} {field_names})" + ); Some(ctr_text) } From c428ebc96706a6d92e05a9f91cf8854a7d23ff17 Mon Sep 17 00:00:00 2001 From: Eduardo Sandalo Porto Date: Tue, 9 Apr 2024 10:26:00 -0300 Subject: [PATCH 06/15] Format type indices into construtors, finishing constructor generation TODO: Test with full `book` --- src/sugar/mod.rs | 29 ++++++++++++++++++++--------- 1 file changed, 20 insertions(+), 9 deletions(-) diff --git a/src/sugar/mod.rs b/src/sugar/mod.rs index 87b65b3..4d3de0c 100644 --- a/src/sugar/mod.rs +++ b/src/sugar/mod.rs @@ -665,14 +665,14 @@ impl Term { // TODO: test if it matches all of the implemented book pub fn constructor_code((adt_name, adt_term): (&str, &Term), ctr_ref: &str) -> Option { // Check if `adt_name` really is an ADT - let (adt, adt_typ) = match &adt_term { + let adt = match &adt_term { // Type variables wrap ADTs in Lams Term::Lam { bod, .. } => return Term::constructor_code((adt_name, bod), ctr_ref), // Skip `Ann` and `Src` Term::Ann { val, .. } => return Term::constructor_code((adt_name, val), ctr_ref), Term::Src { val, .. } => return Term::constructor_code((adt_name, val), ctr_ref), // Found an ADT - Term::Slf { typ, .. } => (adt_term.as_adt()?, typ.show()), + Term::Slf { .. } => adt_term.as_adt()?, _ => return None, }; @@ -681,26 +681,37 @@ impl Term { // Search for constructor in ADT let ctr_ref = ctr_ref.trim_end_matches('/'); // last "/" is not part of name let ctr = ctrs.iter().find(|ctr| format!("{adt_name}/{}", ctr.name) == ctr_ref)?.clone(); - let ctr_name = ctr.name; + let ctr_name = &ctr.name; let names = ctrs.into_iter().map(|ctr| ctr.name); - // Generate constructor code - // TODO: what should I do with ctr.idxs? - // let format_idx = ... + // Generate constructor code: + // Type parameters let format_param = |param| format!("<{}>", param); let params = adt.pars.iter().map(format_param).rev().collect::>().join(" "); + // Constructor fields let format_field = |(name, typ): &(String, Term)| format!("({name}: {})", typ.show()); let fields = ctr.flds.iter().map(format_field).collect::>().join(" "); - let format_ctr_name = |ctr_name| format!("λ{ctr_name}"); - let ctr_names = names.map(format_ctr_name).collect::>().join(" "); + // Constructor return type with type parameters and type indices + let mut ctr_typ = vec![adt.name.clone()]; + adt.pars.into_iter().rev().for_each(|par| ctr_typ.push(par)); + ctr.idxs.into_iter().rev().for_each(|idx| ctr_typ.push(idx.show())); + let ctr_typ = format!("({})", ctr_typ.join(" ")); + // Constructor names into Scott-encoding + let format_ctr_lam_name = |ctr_name| format!("λ{ctr_name}"); + let ctr_lam_names = names.map(format_ctr_lam_name).collect::>().join(" "); + + // Fields without their types let field_names = ctr.flds.iter().map(|(name, _)| name.clone()).collect::>().join(" "); + // The result should be in the following format: + // ctr_name P_1 .. P_n (f_1: T_1) .. (f_n: T_n): (adt_name P_1 .. P_n Idx_1 .. Idx_n) = + // ~λP λctr_name_1 .. λctr_name_n (ctr_name f_1 .. f_n) let ctr_text = format!( - "{ctr_name} {params} {fields}: {adt_typ} =\n ~λP {ctr_names} ({ctr_name} {field_names})" + "{ctr_name} {params} {fields}: {ctr_typ} =\n ~λP {ctr_lam_names} ({ctr_name} {field_names})" ); Some(ctr_text) From ac6438b56332c8d17ff079e44b5f8323b4c62abd Mon Sep 17 00:00:00 2001 From: Eduardo Sandalo Porto Date: Tue, 9 Apr 2024 11:12:44 -0300 Subject: [PATCH 07/15] Create folder structure for the constructor if it does not exist --- src/book/mod.rs | 14 +++++++++++--- 1 file changed, 11 insertions(+), 3 deletions(-) diff --git a/src/book/mod.rs b/src/book/mod.rs index a321d19..2806f0e 100644 --- a/src/book/mod.rs +++ b/src/book/mod.rs @@ -82,9 +82,17 @@ impl Book { let maybe_ctr = Term::constructor_code((&def_name, &def_term), &ref_name); if let Some(ctr_code) = maybe_ctr { - let file = format!("{}.kind2", ref_name.trim_end_matches('/')); - std::fs::write(&file, ctr_code) - .map_err(|_| format!("ERROR: could not create file for generated constructor {ref_name}"))?; + let file_name = format!("{}.kind2", ref_name.trim_end_matches('/')); + let file_path = std::path::Path::new(&file_name); + let err = || format!("ERROR: could not create file for generated constructor {ref_name}"); + + // Create folder structure + std::fs::create_dir_all(file_path.parent().ok_or_else(err)?).map_err(|_| err())?; + // Write constructor to its own file + // TODO: What should I do when the file already exists? + // TODO: If the ADT definition does not type check, the wrong constructor + // is still written to its own file. What should I do in this case? + std::fs::write(&file_name, ctr_code).map_err(|_| err())?; self.load(&base, &ref_name)?; continue; From b8a382c586fb0e5cad450489ef28b39ec0f6945f Mon Sep 17 00:00:00 2001 From: Eduardo Sandalo Porto Date: Tue, 9 Apr 2024 11:50:05 -0300 Subject: [PATCH 08/15] Improve description of the constructor generation result --- src/sugar/mod.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/sugar/mod.rs b/src/sugar/mod.rs index 4d3de0c..b393812 100644 --- a/src/sugar/mod.rs +++ b/src/sugar/mod.rs @@ -708,7 +708,7 @@ impl Term { let field_names = ctr.flds.iter().map(|(name, _)| name.clone()).collect::>().join(" "); // The result should be in the following format: - // ctr_name P_1 .. P_n (f_1: T_1) .. (f_n: T_n): (adt_name P_1 .. P_n Idx_1 .. Idx_n) = + // ctr_name .. (f_1: T_1) .. (f_n: T_n): (adt_name Par_1 .. Par_n Idx_1 .. Idx_n) = // ~λP λctr_name_1 .. λctr_name_n (ctr_name f_1 .. f_n) let ctr_text = format!( "{ctr_name} {params} {fields}: {ctr_typ} =\n ~λP {ctr_lam_names} ({ctr_name} {field_names})" From c11e0819cbf7dbf1e5fe17f3f949fb6663d29952 Mon Sep 17 00:00:00 2001 From: Eduardo Sandalo Porto Date: Tue, 9 Apr 2024 12:41:44 -0300 Subject: [PATCH 09/15] Solve one of the TODO questions --- src/book/mod.rs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/book/mod.rs b/src/book/mod.rs index 2806f0e..3276b8d 100644 --- a/src/book/mod.rs +++ b/src/book/mod.rs @@ -88,8 +88,8 @@ impl Book { // Create folder structure std::fs::create_dir_all(file_path.parent().ok_or_else(err)?).map_err(|_| err())?; - // Write constructor to its own file - // TODO: What should I do when the file already exists? + // Write constructor to its own file. + // It rewrites the file if it already exists. // TODO: If the ADT definition does not type check, the wrong constructor // is still written to its own file. What should I do in this case? std::fs::write(&file_name, ctr_code).map_err(|_| err())?; From 735628816ffecca901c6acb5ba5cf79f112639ad Mon Sep 17 00:00:00 2001 From: Eduardo Sandalo Porto Date: Tue, 9 Apr 2024 22:23:32 -0300 Subject: [PATCH 10/15] Start testing constructor generation MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit TODO: deal with cases like this: ``` assertion `left == right` failed left: "λn ~λP λsucc λzero (succ n)" right: "λpred ~λP λsucc λzero (succ pred)" ``` --- src/book/mod.rs | 50 +++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 50 insertions(+) diff --git a/src/book/mod.rs b/src/book/mod.rs index 3276b8d..9a3dced 100644 --- a/src/book/mod.rs +++ b/src/book/mod.rs @@ -141,3 +141,53 @@ impl Book { } } + +#[cfg(test)] +mod tests { + use crate::*; + + #[test] + /// Test if construction generation matches book + fn constructor_generation() { + let book_dir = PathBuf::from(env!("CARGO_MANIFEST_DIR")).join("book"); + let book = Book::boot(&book_dir.to_string_lossy(), "Test").unwrap(); + + for (_, term) in book.defs.iter() { + fn extract_adt(t: &Term) -> &Term { + match t { + Term::Lam { bod, .. } => extract_adt(bod), + Term::Ann { val, .. } => extract_adt(val), + Term::Src { val, .. } => extract_adt(val), + // Found ADT + Term::Slf { .. } => t, + // Couldn't find ADT + _ => t, + } + } + + if let Some(adt) = extract_adt(term).as_adt() { + let full_name = |adt_name: &str, ctr_name: &str| format!("{adt_name}/{ctr_name}"); + + let ctrs: Vec<(&str, &Term)> = adt + .ctrs + .iter() + .map(|ctr| (ctr.name.as_ref(), &book.defs[&full_name(&adt.name, &ctr.name)])) + .collect(); + + for (ctr_name, ctr_term) in ctrs { + println!("{ctr_name} = {}", ctr_term.show()); + + let ctr_ref = full_name(&adt.name, ctr_name); + let gen_code = Term::constructor_code((&adt.name, term), &ctr_ref).unwrap(); + let gen_term = KindParser::new(&gen_code).parse_def(0, &im::HashMap::new()).unwrap().1; + + // TODO: deal with cases like this: + // assertion `left == right` failed + // left: "λn ~λP λsucc λzero (succ n)" + // right: "λpred ~λP λsucc λzero (succ pred)" + assert_eq!(ctr_term.show(), gen_term.show()); + } + } + } + } +} From 67ea1e648cb56f6730a67e05df482d80e01e9de5 Mon Sep 17 00:00:00 2001 From: Eduardo Sandalo Porto Date: Wed, 10 Apr 2024 13:11:30 -0300 Subject: [PATCH 11/15] Add test for constructor generation TODO: Change test to loop through the entire book --- src/book/mod.rs | 101 +++++++++++++++++++++++++++++++++++++++--------- 1 file changed, 82 insertions(+), 19 deletions(-) diff --git a/src/book/mod.rs b/src/book/mod.rs index 9a3dced..d818bc1 100644 --- a/src/book/mod.rs +++ b/src/book/mod.rs @@ -146,25 +146,92 @@ impl Book { mod tests { use crate::*; + // TODO: this could be in the `sugar` module + fn extract_adt(t: &Term) -> &Term { + match t { + Term::Lam { bod, .. } => extract_adt(bod), + Term::Ann { val, .. } => extract_adt(val), + Term::Src { val, .. } => extract_adt(val), + // Found ADT + Term::Slf { .. } => t, + // Couldn't find ADT + _ => t, + } + } + + // TODO: this could be in the `term` module + fn apply(t: &Term, f: impl Fn(&Term) -> Term) -> Term { + match t { + Term::All { era, nam, inp, bod } => { + Term::All { era: *era, nam: nam.clone(), inp: Box::new(f(inp)), bod: Box::new(f(bod)) } + } + Term::Lam { era, nam, bod } => Term::Lam { era: *era, nam: nam.clone(), bod: Box::new(f(bod)) }, + Term::App { era, fun, arg } => Term::App { era: *era, fun: Box::new(f(fun)), arg: Box::new(f(arg)) }, + Term::Ann { chk, val, typ } => Term::Ann { chk: *chk, val: Box::new(f(val)), typ: Box::new(f(typ)) }, + Term::Slf { nam, typ, bod } => { + Term::Slf { nam: nam.clone(), typ: Box::new(f(typ)), bod: Box::new(f(bod)) } + } + Term::Ins { val } => Term::Ins { val: Box::new(f(val)) }, + Term::Set => Term::Set, + Term::U60 => Term::U60, + Term::Num { val } => Term::Num { val: *val }, + Term::Op2 { opr, fst, snd } => Term::Op2 { opr: *opr, fst: Box::new(f(fst)), snd: Box::new(f(snd)) }, + Term::Swi { nam, x, z, s, p } => Term::Swi { + nam: nam.clone(), + x: Box::new(f(x)), + z: Box::new(f(z)), + s: Box::new(f(s)), + p: Box::new(f(p)), + }, + Term::Nat { nat } => Term::Nat { nat: *nat }, + Term::Txt { txt } => Term::Txt { txt: txt.clone() }, + Term::Let { nam, val, bod } => { + Term::Let { nam: nam.clone(), val: Box::new(f(val)), bod: Box::new(f(bod)) } + } + Term::Use { nam, val, bod } => { + Term::Use { nam: nam.clone(), val: Box::new(f(val)), bod: Box::new(f(bod)) } + } + Term::Var { nam } => Term::Var { nam: nam.clone() }, + Term::Hol { nam } => Term::Hol { nam: nam.clone() }, + Term::Met {} => Term::Met {}, + Term::Src { src, val } => Term::Src { src: src.clone(), val: Box::new(f(val)) }, + Term::Mch { mch } => f(&Term::new_match(mch)), + } + } + + // TODO: this could be used to implement term equality + fn rename_variables(t: &Term, i: usize, uses: &Uses) -> Term { + match t { + Term::Lam { era, nam, bod } => match uses.get(nam) { + Some(nam) => Term::Lam { + era: *era, + nam: nam.clone(), + bod: Box::new(rename_variables(bod, i, uses)), + }, + None => { + let new_nam = format!("x{i}"); + Term::Lam { + era: *era, + nam: new_nam.clone(), + bod: Box::new(rename_variables(bod, i + 1, &uses.update(nam.clone(), new_nam.clone()))), + } + } + }, + Term::Var { nam } => { + Term::Var { nam: uses.get(nam).unwrap_or(nam).clone() } + } + _ => apply(t, |t| rename_variables(t, i, uses)), + } + } + #[test] /// Test if construction generation matches book fn constructor_generation() { let book_dir = PathBuf::from(env!("CARGO_MANIFEST_DIR")).join("book"); + // TODO: test with all books instead of only "Test" let book = Book::boot(&book_dir.to_string_lossy(), "Test").unwrap(); for (_, term) in book.defs.iter() { - fn extract_adt(t: &Term) -> &Term { - match t { - Term::Lam { bod, .. } => extract_adt(bod), - Term::Ann { val, .. } => extract_adt(val), - Term::Src { val, .. } => extract_adt(val), - // Found ADT - Term::Slf { .. } => t, - // Couldn't find ADT - _ => t, - } - } - if let Some(adt) = extract_adt(term).as_adt() { let full_name = |adt_name: &str, ctr_name: &str| format!("{adt_name}/{ctr_name}"); @@ -175,17 +242,13 @@ mod tests { .collect(); for (ctr_name, ctr_term) in ctrs { - println!("{ctr_name} = {}", ctr_term.show()); - let ctr_ref = full_name(&adt.name, ctr_name); let gen_code = Term::constructor_code((&adt.name, term), &ctr_ref).unwrap(); let gen_term = KindParser::new(&gen_code).parse_def(0, &im::HashMap::new()).unwrap().1; - // TODO: deal with cases like this: - // assertion `left == right` failed - // left: "λn ~λP λsucc λzero (succ n)" - // right: "λpred ~λP λsucc λzero (succ pred)" - assert_eq!(ctr_term.show(), gen_term.show()); + let t1 = rename_variables(ctr_term, 0, &im::HashMap::new()); + let t2 = rename_variables(&gen_term, 0, &im::HashMap::new()); + assert_eq!(t1.show(), t2.show()); } } } From 258104ad48ff977f3ded86f44cbc369578048635 Mon Sep 17 00:00:00 2001 From: Eduardo Sandalo Porto Date: Wed, 10 Apr 2024 21:43:22 -0300 Subject: [PATCH 12/15] (Mostly) fully test constructor generation A few modules were selected to compare their constructors with the generated ones. --- src/book/mod.rs | 58 ++++++++++++++++++++++++++++++------------------ src/sugar/mod.rs | 1 - 2 files changed, 36 insertions(+), 23 deletions(-) diff --git a/src/book/mod.rs b/src/book/mod.rs index d818bc1..16408ed 100644 --- a/src/book/mod.rs +++ b/src/book/mod.rs @@ -206,20 +206,18 @@ mod tests { Some(nam) => Term::Lam { era: *era, nam: nam.clone(), - bod: Box::new(rename_variables(bod, i, uses)), + bod: Box::new(rename_variables(bod, i, uses)) }, None => { let new_nam = format!("x{i}"); Term::Lam { era: *era, nam: new_nam.clone(), - bod: Box::new(rename_variables(bod, i + 1, &uses.update(nam.clone(), new_nam.clone()))), + bod: Box::new(rename_variables(bod, i + 1, &uses.update(nam.clone(), new_nam))), } } }, - Term::Var { nam } => { - Term::Var { nam: uses.get(nam).unwrap_or(nam).clone() } - } + Term::Var { nam } => Term::Var { nam: uses.get(nam).unwrap_or(nam).clone() }, _ => apply(t, |t| rename_variables(t, i, uses)), } } @@ -228,29 +226,45 @@ mod tests { /// Test if construction generation matches book fn constructor_generation() { let book_dir = PathBuf::from(env!("CARGO_MANIFEST_DIR")).join("book"); - // TODO: test with all books instead of only "Test" - let book = Book::boot(&book_dir.to_string_lossy(), "Test").unwrap(); + let modules_to_test = [ + "BBT", "BMap", "Bool", "Char", "Cmp", "Empty", "Equal", "List", "Maybe", "Monad", "Nat", "Pair", + "String", "Vector", + ]; + + for module in modules_to_test { + println!("Testing module `{module}`."); + let mut book = Book::boot(&book_dir.to_string_lossy(), module).unwrap(); + // Needed because some constructors are loaded as ADT.cons instead of ADT/cons + book.defs = book.defs.into_iter().map(|(key, val)| (key.replace(".", "/"), val)).collect(); - for (_, term) in book.defs.iter() { - if let Some(adt) = extract_adt(term).as_adt() { - let full_name = |adt_name: &str, ctr_name: &str| format!("{adt_name}/{ctr_name}"); + for (_, term) in book.defs.iter() { + if let Some(adt) = extract_adt(term).as_adt() { + println!("Testing ADT `{}`.", adt.name); + let full_name = |adt_name: &str, ctr_name: &str| format!("{adt_name}/{ctr_name}"); - let ctrs: Vec<(&str, &Term)> = adt - .ctrs - .iter() - .map(|ctr| (ctr.name.as_ref(), &book.defs[&full_name(&adt.name, &ctr.name)])) - .collect(); + let ctrs: Vec<(&str, &Term)> = adt + .ctrs + .iter() + .map(|ctr| { + let name = full_name(&adt.name, &ctr.name); + (ctr.name.as_ref(), book.defs.get(&name).expect(&format!("couldn't find {name}"))) + }) + .collect(); - for (ctr_name, ctr_term) in ctrs { - let ctr_ref = full_name(&adt.name, ctr_name); - let gen_code = Term::constructor_code((&adt.name, term), &ctr_ref).unwrap(); - let gen_term = KindParser::new(&gen_code).parse_def(0, &im::HashMap::new()).unwrap().1; + for (ctr_name, ctr_term) in ctrs { + println!("Testing constructor {ctr_name}"); + + let ctr_ref = full_name(&adt.name, ctr_name); + let gen_code = Term::constructor_code((&adt.name, term), &ctr_ref).unwrap(); + let gen_term = KindParser::new(&gen_code).parse_def(0, &im::HashMap::new()).unwrap().1; - let t1 = rename_variables(ctr_term, 0, &im::HashMap::new()); - let t2 = rename_variables(&gen_term, 0, &im::HashMap::new()); - assert_eq!(t1.show(), t2.show()); + let t1 = rename_variables(ctr_term, 0, &im::HashMap::new()); + let t2 = rename_variables(&gen_term, 0, &im::HashMap::new()); + assert_eq!(t1.show(), t2.show()); + } } } + println!(); } } } diff --git a/src/sugar/mod.rs b/src/sugar/mod.rs index b393812..ca4e72d 100644 --- a/src/sugar/mod.rs +++ b/src/sugar/mod.rs @@ -662,7 +662,6 @@ impl Term { return term; } - // TODO: test if it matches all of the implemented book pub fn constructor_code((adt_name, adt_term): (&str, &Term), ctr_ref: &str) -> Option { // Check if `adt_name` really is an ADT let adt = match &adt_term { From 63f0dc3466551e1ad27f6056618dc841cf67d9db Mon Sep 17 00:00:00 2001 From: Eduardo Sandalo Porto Date: Thu, 11 Apr 2024 16:10:49 -0300 Subject: [PATCH 13/15] Test nested module --- book/Nested/Test.kind2 | 4 ++++ book/Nested/Test/ctr1.kind2 | 2 ++ book/Nested/Test/ctr2.kind2 | 2 ++ src/book/mod.rs | 2 +- 4 files changed, 9 insertions(+), 1 deletion(-) create mode 100644 book/Nested/Test.kind2 create mode 100644 book/Nested/Test/ctr1.kind2 create mode 100644 book/Nested/Test/ctr2.kind2 diff --git a/book/Nested/Test.kind2 b/book/Nested/Test.kind2 new file mode 100644 index 0000000..40ffccb --- /dev/null +++ b/book/Nested/Test.kind2 @@ -0,0 +1,4 @@ +data Nested/Test T Z +| ctr1 : (Nested/Test T Z) +| ctr2 : (Nested/Test T Z) + diff --git a/book/Nested/Test/ctr1.kind2 b/book/Nested/Test/ctr1.kind2 new file mode 100644 index 0000000..d2dbb91 --- /dev/null +++ b/book/Nested/Test/ctr1.kind2 @@ -0,0 +1,2 @@ +ctr1 : (Nested/Test T Z) = + ~λP λctr1 λctr2 (ctr1 ) \ No newline at end of file diff --git a/book/Nested/Test/ctr2.kind2 b/book/Nested/Test/ctr2.kind2 new file mode 100644 index 0000000..8430081 --- /dev/null +++ b/book/Nested/Test/ctr2.kind2 @@ -0,0 +1,2 @@ +ctr2 : (Nested/Test T Z) = + ~λP λctr1 λctr2 (ctr2 ) \ No newline at end of file diff --git a/src/book/mod.rs b/src/book/mod.rs index 16408ed..ec3a0b6 100644 --- a/src/book/mod.rs +++ b/src/book/mod.rs @@ -228,7 +228,7 @@ mod tests { let book_dir = PathBuf::from(env!("CARGO_MANIFEST_DIR")).join("book"); let modules_to_test = [ "BBT", "BMap", "Bool", "Char", "Cmp", "Empty", "Equal", "List", "Maybe", "Monad", "Nat", "Pair", - "String", "Vector", + "String", "Vector", "Nested/Test" ]; for module in modules_to_test { From af819567fd69ed990224a43038d90752a03747ad Mon Sep 17 00:00:00 2001 From: Eduardo Sandalo Porto Date: Thu, 11 Apr 2024 17:52:12 -0300 Subject: [PATCH 14/15] Add specific Kind2 tests for constructor generation --- book/Nested/Test.kind2 | 4 ---- book/Nested/Test/ctr1.kind2 | 2 -- book/Nested/Test/ctr2.kind2 | 2 -- book/Tests/CtrGen/ParamsTest.kind2 | 3 +++ book/Tests/CtrGen/ParamsTest/ctr1.kind2 | 2 ++ book/Tests/CtrGen/ParamsTest/ctr2.kind2 | 2 ++ book/Tests/CtrGen/VectorTest.kind2 | 6 ++++++ book/Tests/CtrGen/VectorTest/cons.kind2 | 2 ++ book/Tests/CtrGen/VectorTest/nil.kind2 | 2 ++ src/book/mod.rs | 2 +- 10 files changed, 18 insertions(+), 9 deletions(-) delete mode 100644 book/Nested/Test.kind2 delete mode 100644 book/Nested/Test/ctr1.kind2 delete mode 100644 book/Nested/Test/ctr2.kind2 create mode 100644 book/Tests/CtrGen/ParamsTest.kind2 create mode 100644 book/Tests/CtrGen/ParamsTest/ctr1.kind2 create mode 100644 book/Tests/CtrGen/ParamsTest/ctr2.kind2 create mode 100644 book/Tests/CtrGen/VectorTest.kind2 create mode 100644 book/Tests/CtrGen/VectorTest/cons.kind2 create mode 100644 book/Tests/CtrGen/VectorTest/nil.kind2 diff --git a/book/Nested/Test.kind2 b/book/Nested/Test.kind2 deleted file mode 100644 index 40ffccb..0000000 --- a/book/Nested/Test.kind2 +++ /dev/null @@ -1,4 +0,0 @@ -data Nested/Test T Z -| ctr1 : (Nested/Test T Z) -| ctr2 : (Nested/Test T Z) - diff --git a/book/Nested/Test/ctr1.kind2 b/book/Nested/Test/ctr1.kind2 deleted file mode 100644 index d2dbb91..0000000 --- a/book/Nested/Test/ctr1.kind2 +++ /dev/null @@ -1,2 +0,0 @@ -ctr1 : (Nested/Test T Z) = - ~λP λctr1 λctr2 (ctr1 ) \ No newline at end of file diff --git a/book/Nested/Test/ctr2.kind2 b/book/Nested/Test/ctr2.kind2 deleted file mode 100644 index 8430081..0000000 --- a/book/Nested/Test/ctr2.kind2 +++ /dev/null @@ -1,2 +0,0 @@ -ctr2 : (Nested/Test T Z) = - ~λP λctr1 λctr2 (ctr2 ) \ No newline at end of file diff --git a/book/Tests/CtrGen/ParamsTest.kind2 b/book/Tests/CtrGen/ParamsTest.kind2 new file mode 100644 index 0000000..98df41e --- /dev/null +++ b/book/Tests/CtrGen/ParamsTest.kind2 @@ -0,0 +1,3 @@ +data Tests/CtrGen/ParamsTest T Z +| ctr1 : (Tests/CtrGen/ParamsTest T Z) +| ctr2 : (Tests/CtrGen/ParamsTest T Z) diff --git a/book/Tests/CtrGen/ParamsTest/ctr1.kind2 b/book/Tests/CtrGen/ParamsTest/ctr1.kind2 new file mode 100644 index 0000000..3a4b4e2 --- /dev/null +++ b/book/Tests/CtrGen/ParamsTest/ctr1.kind2 @@ -0,0 +1,2 @@ +ctr1 : (Tests/CtrGen/ParamsTest T Z) = + ~λP λctr1 λctr2 (ctr1 ) \ No newline at end of file diff --git a/book/Tests/CtrGen/ParamsTest/ctr2.kind2 b/book/Tests/CtrGen/ParamsTest/ctr2.kind2 new file mode 100644 index 0000000..cf1c103 --- /dev/null +++ b/book/Tests/CtrGen/ParamsTest/ctr2.kind2 @@ -0,0 +1,2 @@ +ctr2 : (Tests/CtrGen/ParamsTest T Z) = + ~λP λctr1 λctr2 (ctr2 ) \ No newline at end of file diff --git a/book/Tests/CtrGen/VectorTest.kind2 b/book/Tests/CtrGen/VectorTest.kind2 new file mode 100644 index 0000000..6533cfb --- /dev/null +++ b/book/Tests/CtrGen/VectorTest.kind2 @@ -0,0 +1,6 @@ +data Tests/CtrGen/VectorTest T (len: Nat) +| cons (len: Nat) + (head: T) + (tail: (Tests/CtrGen/VectorTest T len)) : + (Tests/CtrGen/VectorTest T (Nat/succ len)) +| nil : (Tests/CtrGen/VectorTest T Nat/zero) diff --git a/book/Tests/CtrGen/VectorTest/cons.kind2 b/book/Tests/CtrGen/VectorTest/cons.kind2 new file mode 100644 index 0000000..07c4475 --- /dev/null +++ b/book/Tests/CtrGen/VectorTest/cons.kind2 @@ -0,0 +1,2 @@ +cons (len: Nat) (head: T) (tail: (Tests/CtrGen/VectorTest T len)): (Tests/CtrGen/VectorTest T (Nat/succ len)) = + ~λP λcons λnil (cons len head tail) \ No newline at end of file diff --git a/book/Tests/CtrGen/VectorTest/nil.kind2 b/book/Tests/CtrGen/VectorTest/nil.kind2 new file mode 100644 index 0000000..ef3c76e --- /dev/null +++ b/book/Tests/CtrGen/VectorTest/nil.kind2 @@ -0,0 +1,2 @@ +nil : (Tests/CtrGen/VectorTest T Nat/zero) = + ~λP λcons λnil (nil ) \ No newline at end of file diff --git a/src/book/mod.rs b/src/book/mod.rs index ec3a0b6..fbd1fdc 100644 --- a/src/book/mod.rs +++ b/src/book/mod.rs @@ -228,7 +228,7 @@ mod tests { let book_dir = PathBuf::from(env!("CARGO_MANIFEST_DIR")).join("book"); let modules_to_test = [ "BBT", "BMap", "Bool", "Char", "Cmp", "Empty", "Equal", "List", "Maybe", "Monad", "Nat", "Pair", - "String", "Vector", "Nested/Test" + "String", "Vector", "Tests/CtrGen/ParamsTest", "Tests/CtrGen/VectorTest" ]; for module in modules_to_test { From 67abc5cdf8738ef9aa541204e03cf8b060776844 Mon Sep 17 00:00:00 2001 From: Eduardo Sandalo Porto Date: Thu, 11 Apr 2024 20:18:54 -0300 Subject: [PATCH 15/15] Refactor code generation to use `Show` --- book/Tests/CtrGen/ParamsTest/ctr1.kind2 | 4 +- book/Tests/CtrGen/ParamsTest/ctr2.kind2 | 4 +- book/Tests/CtrGen/VectorTest/cons.kind2 | 4 +- book/Tests/CtrGen/VectorTest/nil.kind2 | 4 +- src/book/mod.rs | 25 ++++++-- src/show/mod.rs | 14 ++++- src/sugar/mod.rs | 81 +++++++++++++++++-------- 7 files changed, 97 insertions(+), 39 deletions(-) diff --git a/book/Tests/CtrGen/ParamsTest/ctr1.kind2 b/book/Tests/CtrGen/ParamsTest/ctr1.kind2 index 3a4b4e2..d663fcc 100644 --- a/book/Tests/CtrGen/ParamsTest/ctr1.kind2 +++ b/book/Tests/CtrGen/ParamsTest/ctr1.kind2 @@ -1,2 +1,2 @@ -ctr1 : (Tests/CtrGen/ParamsTest T Z) = - ~λP λctr1 λctr2 (ctr1 ) \ No newline at end of file +ctr1 : (Tests/CtrGen/ParamsTest T Z) = + ~λP λctr1 λctr2 (ctr1) \ No newline at end of file diff --git a/book/Tests/CtrGen/ParamsTest/ctr2.kind2 b/book/Tests/CtrGen/ParamsTest/ctr2.kind2 index cf1c103..a755586 100644 --- a/book/Tests/CtrGen/ParamsTest/ctr2.kind2 +++ b/book/Tests/CtrGen/ParamsTest/ctr2.kind2 @@ -1,2 +1,2 @@ -ctr2 : (Tests/CtrGen/ParamsTest T Z) = - ~λP λctr1 λctr2 (ctr2 ) \ No newline at end of file +ctr2 : (Tests/CtrGen/ParamsTest T Z) = + ~λP λctr1 λctr2 (ctr2) \ No newline at end of file diff --git a/book/Tests/CtrGen/VectorTest/cons.kind2 b/book/Tests/CtrGen/VectorTest/cons.kind2 index 07c4475..e07ca9f 100644 --- a/book/Tests/CtrGen/VectorTest/cons.kind2 +++ b/book/Tests/CtrGen/VectorTest/cons.kind2 @@ -1,2 +1,2 @@ -cons (len: Nat) (head: T) (tail: (Tests/CtrGen/VectorTest T len)): (Tests/CtrGen/VectorTest T (Nat/succ len)) = - ~λP λcons λnil (cons len head tail) \ No newline at end of file +cons (len: Nat) (head: T) (tail: (Tests/CtrGen/VectorTest T len)) : (Tests/CtrGen/VectorTest T (Nat/succ len)) = + ~λP λcons λnil (cons len head tail) \ No newline at end of file diff --git a/book/Tests/CtrGen/VectorTest/nil.kind2 b/book/Tests/CtrGen/VectorTest/nil.kind2 index ef3c76e..5baf03c 100644 --- a/book/Tests/CtrGen/VectorTest/nil.kind2 +++ b/book/Tests/CtrGen/VectorTest/nil.kind2 @@ -1,2 +1,2 @@ -nil : (Tests/CtrGen/VectorTest T Nat/zero) = - ~λP λcons λnil (nil ) \ No newline at end of file +nil : (Tests/CtrGen/VectorTest T Nat/zero) = + ~λP λcons λnil (nil) \ No newline at end of file diff --git a/src/book/mod.rs b/src/book/mod.rs index fbd1fdc..ca3bf22 100644 --- a/src/book/mod.rs +++ b/src/book/mod.rs @@ -82,6 +82,8 @@ impl Book { let maybe_ctr = Term::constructor_code((&def_name, &def_term), &ref_name); if let Some(ctr_code) = maybe_ctr { + let ctr_code = ctr_code.flatten(Some(80)); + let file_name = format!("{}.kind2", ref_name.trim_end_matches('/')); let file_path = std::path::Path::new(&file_name); let err = || format!("ERROR: could not create file for generated constructor {ref_name}"); @@ -227,8 +229,22 @@ mod tests { fn constructor_generation() { let book_dir = PathBuf::from(env!("CARGO_MANIFEST_DIR")).join("book"); let modules_to_test = [ - "BBT", "BMap", "Bool", "Char", "Cmp", "Empty", "Equal", "List", "Maybe", "Monad", "Nat", "Pair", - "String", "Vector", "Tests/CtrGen/ParamsTest", "Tests/CtrGen/VectorTest" + "BBT", + "BMap", + "Bool", + "Char", + "Cmp", + "Empty", + "Equal", + "List", + "Maybe", + "Monad", + "Nat", + "Pair", + "String", + "Vector", + "Tests/CtrGen/ParamsTest", + "Tests/CtrGen/VectorTest", ]; for module in modules_to_test { @@ -253,10 +269,11 @@ mod tests { for (ctr_name, ctr_term) in ctrs { println!("Testing constructor {ctr_name}"); - + let ctr_ref = full_name(&adt.name, ctr_name); let gen_code = Term::constructor_code((&adt.name, term), &ctr_ref).unwrap(); - let gen_term = KindParser::new(&gen_code).parse_def(0, &im::HashMap::new()).unwrap().1; + let gen_term = + KindParser::new(&gen_code.flatten(None)).parse_def(0, &im::HashMap::new()).unwrap().1; let t1 = rename_variables(ctr_term, 0, &im::HashMap::new()); let t2 = rename_variables(&gen_term, 0, &im::HashMap::new()); diff --git a/src/show/mod.rs b/src/show/mod.rs index 19b062d..568fc9c 100644 --- a/src/show/mod.rs +++ b/src/show/mod.rs @@ -128,7 +128,7 @@ impl Show { }, Style::Glue => { for (i, c) in child.iter().enumerate() { - if i > 0 { + if i > 0 && !c.is_empty() { out.push_str(&join); } c.flatten_into(out, fmt, tab, lim); @@ -162,6 +162,18 @@ impl Show { } } + // Checks if the element contains no text. + fn is_empty(&self) -> bool { + match self { + Show::Many { child, .. } => child.is_empty(), + Show::Text { value } => value.is_empty(), + Show::Line => false, + Show::Semi => false, + Show::Inc => false, + Show::Dec => false, + } + } + // Sums the width of all children ropes, up to a limit. fn width(&self, lim: usize) -> usize { let mut total_width = 0; diff --git a/src/sugar/mod.rs b/src/sugar/mod.rs index ca4e72d..7e6fb55 100644 --- a/src/sugar/mod.rs +++ b/src/sugar/mod.rs @@ -394,7 +394,6 @@ impl<'i> KindParser<'i> { // --- impl Term { - // Interprets a λ-encoded Algebraic Data Type definition as an ADT struct. pub fn as_adt(&self) -> Option { let name: String; @@ -662,7 +661,7 @@ impl Term { return term; } - pub fn constructor_code((adt_name, adt_term): (&str, &Term), ctr_ref: &str) -> Option { + pub fn constructor_code((adt_name, adt_term): (&str, &Term), ctr_ref: &str) -> Option> { // Check if `adt_name` really is an ADT let adt = match &adt_term { // Type variables wrap ADTs in Lams @@ -680,38 +679,68 @@ impl Term { // Search for constructor in ADT let ctr_ref = ctr_ref.trim_end_matches('/'); // last "/" is not part of name let ctr = ctrs.iter().find(|ctr| format!("{adt_name}/{}", ctr.name) == ctr_ref)?.clone(); - let ctr_name = &ctr.name; - let names = ctrs.into_iter().map(|ctr| ctr.name); // Generate constructor code: - // Type parameters - let format_param = |param| format!("<{}>", param); - let params = adt.pars.iter().map(format_param).rev().collect::>().join(" "); - - // Constructor fields - let format_field = |(name, typ): &(String, Term)| format!("({name}: {})", typ.show()); - let fields = ctr.flds.iter().map(format_field).collect::>().join(" "); - - // Constructor return type with type parameters and type indices - let mut ctr_typ = vec![adt.name.clone()]; - adt.pars.into_iter().rev().for_each(|par| ctr_typ.push(par)); - ctr.idxs.into_iter().rev().for_each(|idx| ctr_typ.push(idx.show())); - let ctr_typ = format!("({})", ctr_typ.join(" ")); - - // Constructor names into Scott-encoding - let format_ctr_lam_name = |ctr_name| format!("λ{ctr_name}"); - let ctr_lam_names = names.map(format_ctr_lam_name).collect::>().join(" "); + // Constructor name. + let ctr_name = &ctr.name; - // Fields without their types - let field_names = ctr.flds.iter().map(|(name, _)| name.clone()).collect::>().join(" "); + // Type parameters. + // Format: .. + let format_param = |param| Show::text(&format!("<{}>", param)); + let params = Show::glue(" ", adt.pars.iter().map(format_param).rev().collect()); + + // Constructor fields. + // Format: (f_1: T_1) .. (f_n: T_n) + let format_field = |(name, typ): &(String, Term)| { + Show::glue("", vec![ + Show::text("("), + Show::glue("", vec![Show::text(name), Show::text(": "), typ.format()]), + Show::text(")"), + ]) + }; + let fields = Show::glue(" ", ctr.flds.iter().map(format_field).collect()); + + // Constructor return type with type parameters and type indices. + // Format: (adt_name Par_1 .. Par_n Idx_1 .. Idx_n) + let mut ctr_typ = vec![Show::text(&adt.name)]; + adt.pars.iter().rev().for_each(|par| ctr_typ.push(Show::text(par))); + ctr.idxs.iter().rev().for_each(|idx| ctr_typ.push(idx.format())); + let ctr_typ = Show::glue("", vec![Show::text("("), Show::glue(" ", ctr_typ), Show::text(")")]); + + // Constructor names into Scott-encoding. + // Format: λctr_name_1 .. λctr_name_n + let format_ctr_lam_name = |ctr_name| Show::text(&format!("λ{ctr_name}")); + let names = ctrs.into_iter().map(|ctr| ctr.name); + let ctr_lam_names = Show::glue(" ", names.map(format_ctr_lam_name).collect()); + + // Fields without their types. + // Format: f_1 .. f_n + let field_names = Show::glue(" ", ctr.flds.iter().map(|(name, _)| Show::text(name)).collect()); + + // Applies constructor and fields. + // Format: (ctr_name f_1 .. f_n) + let final_app = Show::glue("", vec![ + Show::text("("), + Show::glue(" ", vec![Show::text(ctr_name), field_names]), + Show::text(")"), + ]); // The result should be in the following format: // ctr_name .. (f_1: T_1) .. (f_n: T_n): (adt_name Par_1 .. Par_n Idx_1 .. Idx_n) = // ~λP λctr_name_1 .. λctr_name_n (ctr_name f_1 .. f_n) - let ctr_text = format!( - "{ctr_name} {params} {fields}: {ctr_typ} =\n ~λP {ctr_lam_names} ({ctr_name} {field_names})" - ); + let ctr_text = Show::glue(" ", vec![ + Show::text(ctr_name), + params, + fields, + Show::text(":"), + ctr_typ, + Show::text("="), + Show::line(), + Show::text("~λP"), + ctr_lam_names, + final_app, + ]); Some(ctr_text) }