diff --git a/src/fun/net_to_term.rs b/src/fun/net_to_term.rs index 3b8f80bb..ec56b953 100644 --- a/src/fun/net_to_term.rs +++ b/src/fun/net_to_term.rs @@ -144,7 +144,7 @@ impl Reader<'_> { let zero_term = self.read_term(self.net.enter_port(Port(sel_node, 1))); let mut succ_term = self.read_term(self.net.enter_port(Port(sel_node, 2))); // Call expand_generated in case of succ_term be a lifted term - succ_term.expand_generated(&self.book, &self.recursive_defs); + succ_term.expand_generated(self.book, self.recursive_defs); // Succ term should be a lambda let (zero, succ) = match &mut succ_term { diff --git a/src/fun/transform/encode_adts.rs b/src/fun/transform/encode_adts.rs index a65b0a7c..35183ec4 100644 --- a/src/fun/transform/encode_adts.rs +++ b/src/fun/transform/encode_adts.rs @@ -16,21 +16,11 @@ impl Book { let body = match adt_encoding { AdtEncoding::Scott => encode_ctr_scott(fields.iter().map(|f| &f.nam), ctrs, ctr_name), AdtEncoding::NumScott => { - let is_object = adt_name == ctr_name; - if is_object { - let tag = Name::new(format!("{ctr_name}/tag")); - let body = encode_ctr_num_scott(fields.iter().map(|f| &f.nam), &tag); - let tag_def = make_tag_def(ctr_idx, &tag, adt); - tags.push((tag, tag_def)); - body - } else { - let (typ, ctr) = ctr_name.rsplit_once('/').expect("To split at '/'"); - let tag = Name::new(format!("{typ}/{ctr}/tag")); - let body = encode_ctr_num_scott(fields.iter().map(|f| &f.nam), &tag); - let tag_def = make_tag_def(ctr_idx, &tag, adt); - tags.push((tag, tag_def)); - body - } + let tag = make_tag(adt_name == ctr_name, ctr_name); + let body = encode_ctr_num_scott(fields.iter().map(|f| &f.nam), &tag); + let tag_def = make_tag_def(ctr_idx, &tag, adt); + tags.push((tag, tag_def)); + body } }; @@ -44,6 +34,15 @@ impl Book { } } +fn make_tag(is_object: bool, ctr_name: &Name) -> Name { + if is_object { + Name::new(format!("{ctr_name}/tag")) + } else { + let (typ, ctr) = ctr_name.rsplit_once('/').expect("To split at '/'"); + Name::new(format!("{typ}/{ctr}/tag")) + } +} + fn encode_ctr_scott<'a>( ctr_args: impl DoubleEndedIterator + Clone, ctrs: Vec,