diff --git a/book/Tests/CtrGen/ParamsTest/ctr1.kind2 b/book/Tests/CtrGen/ParamsTest/ctr1.kind2 index 3a4b4e28..d663fcc2 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 cf1c103f..a7555864 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 07c44753..e07ca9fc 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 ef3c76e6..5baf03c9 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 fbd1fdc2..ca3bf226 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 19b062d5..568fc9cf 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 ca4e72de..7e6fb55d 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 name. + let ctr_name = &ctr.name; - // Constructor fields - let format_field = |(name, typ): &(String, Term)| format!("({name}: {})", typ.show()); - let fields = ctr.flds.iter().map(format_field).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 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 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 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 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(")")]); - // Fields without their types - let field_names = ctr.flds.iter().map(|(name, _)| name.clone()).collect::>().join(" "); + // 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) }