Remove unnecessary tail.

src/circuit/circuit_frame.rs

@@ -2858,28 +2858,11 @@ fn reduce_cons<F: LurkField, CS: ConstraintSystem<F>, C: Coprocessor<F>>(
                         &[&g.quote_ptr, &result_expr],
                     )?;
 
-                    let default_num_pair = &[&g.default_num, &g.default_num];
-
-                    // TODO: This should be better abstracted, perhaps by resurrecting historical code.
-                    let tail_components: &[&dyn AsAllocatedHashComponents<F>; 4] = &[
-                        &result_env,
-                        &result_cont,
-                        default_num_pair,
-                        default_num_pair,
-                    ];
-
-                    let tail_cont = AllocatedContPtr::construct(
-                        &mut cs.namespace(|| "coprocessor tail cont"),
-                        store,
-                        &g.tail_cont_tag,
-                        tail_components,
-                    )?;
-
                     let new_expr = pick_ptr!(cs, &arity_is_correct, &quoted_expr, &rest)?; // TODO: The error case should probably be expr, but this is harder in straight evaluation atm.
 
                     let new_env = pick_ptr!(cs, &arity_is_correct, &result_env, &env)?;
                     let new_cont =
-                        pick_cont_ptr!(cs, &arity_is_correct, &tail_cont, &g.error_ptr_cont)?;
+                        pick_cont_ptr!(cs, &arity_is_correct, &result_cont, &g.error_ptr_cont)?;
 
                     // We can't just call `results.add_clauses_cons` here because of lifetime issues.
                     coprocessor_results.push((z_ptr, new_expr, new_env, new_cont, &g.false_num));

src/coprocessor/mod.rs

@@ -6,7 +6,7 @@ use bellpepper_core::{ConstraintSystem, SynthesisError};
 use crate::circuit::circuit_frame::{car_cdr, destructure_list};
 use crate::circuit::gadgets::constraints::{alloc_equal_const, enforce_equal_const};
 use crate::circuit::gadgets::data::GlobalAllocations;
-use crate::circuit::gadgets::pointer::{AllocatedContPtr, AllocatedPtr, AsAllocatedHashComponents};
+use crate::circuit::gadgets::pointer::{AllocatedContPtr, AllocatedPtr};
 use crate::eval::IO;
 use crate::field::LurkField;
 use crate::ptr::{ContPtr, Ptr};
@@ -133,26 +133,12 @@ pub trait Coprocessor<F: LurkField>: Clone + Debug + Sync + Send + CoCircuit<F>
             &[&g.quote_ptr, &result_expr],
         )?;
 
-        let default_num_pair = &[&g.default_num, &g.default_num];
+        // FIXME: technically, the error is defined to be rest -- which is the cdr of input_expr.tes
+        //let new_expr = pick_ptr!(cs, &arity_is_correct, &quoted_expr, &rest)?;
+        let new_expr = pick_ptr!(cs, &arity_is_correct, &quoted_expr, &input_expr)?;
 
-        // TODO: This should be better abstracted, perhaps by resurrecting historical code.
-        let tail_components: &[&dyn AsAllocatedHashComponents<F>; 4] = &[
-            &result_env,
-            &result_cont,
-            default_num_pair,
-            default_num_pair,
-        ];
-
-        let tail_cont = AllocatedContPtr::construct(
-            &mut cs.namespace(|| "coprocessor tail cont"),
-            store,
-            &g.tail_cont_tag,
-            tail_components,
-        )?;
-
-        let new_expr = pick_ptr!(cs, &arity_is_correct, &quoted_expr, &rest)?;
         let new_env = pick_ptr!(cs, &arity_is_correct, &result_env, &input_env)?;
-        let new_cont = pick_cont_ptr!(cs, &arity_is_correct, &tail_cont, &g.error_ptr_cont)?;
+        let new_cont = pick_cont_ptr!(cs, &arity_is_correct, &result_cont, &g.error_ptr_cont)?;
 
         Ok((new_expr, new_env, new_cont))
     }

src/eval/reduction.rs

@@ -574,12 +574,8 @@ fn reduce_with_witness_inner<F: LurkField, C: Coprocessor<F>>(
                             } else {
                                 let quoted = store.list(&[quote, expr]);
 
-                                // NOTE: This will be a potentially redundant tail cont, which is 'okay' as long as circuit does same.
-                                // Alternately, here and in circuit(s), we could use the dynamic logic to avoid.
-                                let tail_cont = make_tail_continuation_raw(env, cont, store);
-
                                 return Ok((
-                                    Control::Return(quoted, env, tail_cont),
+                                    Control::Return(quoted, env, cont),
                                     None,
                                     Meta::Coprocessor(*z_ptr),
                                 ));
@@ -1325,18 +1321,6 @@ fn make_tail_continuation<F: LurkField>(
     // point to one another: they can only be nested one deep.
 }
 
-fn make_tail_continuation_raw<F: LurkField>(
-    saved_env: Ptr<F>,
-    continuation: ContPtr<F>,
-    store: &mut Store<F>,
-) -> ContPtr<F> {
-    Continuation::Tail {
-        saved_env,
-        continuation,
-    }
-    .intern_aux(store)
-}
-
 // Only used in tests. Real evalution should use extend_name.
 #[allow(dead_code)]
 pub(crate) fn extend<F: LurkField>(

src/eval/tests/mod.rs

@@ -2671,7 +2671,7 @@ pub(crate) mod coproc {
             None,
             Some(terminal),
             None,
-            5,
+            4,
             Some(&lang),
         );
         test_aux(s, expr3, None, None, Some(error), None, 1, Some(&lang));

src/eval/tests/trie.rs

@@ -25,7 +25,7 @@ fn trie_lang() {
         None,
         None,
         None,
-        5,
+        4,
         Some(&lang),
     );
 

src/proof/nova.rs

@@ -3950,7 +3950,7 @@ pub mod tests {
         let lang = Arc::new(lang);
 
         test_aux(s, expr, Some(res), None, None, None, 2, Some(lang.clone()));
-        test_aux(s, expr2, Some(res), None, None, None, 5, Some(lang.clone()));
+        test_aux(s, expr2, Some(res), None, None, None, 4, Some(lang.clone()));
         test_aux(
             s,
             expr3,