Simplify ContextStack::push interface

carcara/src/ast/context.rs

@@ -96,13 +96,18 @@ impl ContextStack {
     /// how many contexts there are in the proof (and it's not needed since we
     /// can always add a new context at the end of the vector just like an usual
     /// stack)
-    pub fn force_new_context(&mut self) -> usize {
+    fn force_new_context(&mut self) -> usize {
         let ctx_vec = Arc::get_mut(&mut self.context_vec).unwrap();
         ctx_vec.push((AtomicUsize::new(1), RwLock::new(None)));
         ctx_vec.len() - 1
     }
 
-    pub fn push(&mut self, args: &[AnchorArg], context_id: usize) {
+    pub fn push(&mut self, args: &[AnchorArg]) {
+        let id = self.force_new_context();
+        self.push_with_id(args, id);
+    }
+
+    pub fn push_with_id(&mut self, args: &[AnchorArg], context_id: usize) {
         // The write guard was yielded to this thread
         if let Ok(mut ctx_write_guard) = self.context_vec[context_id].1.try_write() {
             // It's the first thread trying to build this context. It will

carcara/src/checker/mod.rs

@@ -160,8 +160,7 @@ impl<'c> ProofChecker<'c> {
                     let time = Instant::now();
                     let step_id = command.id();
 
-                    let new_context_id = self.context.force_new_context();
-                    self.context.push(&s.args, new_context_id);
+                    self.context.push(&s.args);
 
                     if let Some(elaborator) = &mut self.elaborator {
                         elaborator.open_subproof(s.commands.len());

carcara/src/checker/parallel/mod.rs

@@ -287,7 +287,7 @@ impl<'c> ParallelProofChecker<'c> {
                     let time = Instant::now();
                     let step_id = command.id();
 
-                    self.context.push(&s.args, s.context_id);
+                    self.context.push_with_id(&s.args, s.context_id);
 
                     if let Some(stats) = &mut stats {
                         // Collects statistics

carcara/src/elaborator/polyeq.rs

@@ -121,10 +121,7 @@ impl<'a> PolyeqElaborator<'a> {
                             });
 
                         let args: Vec<_> = variable_args.chain(assign_args).collect();
-
-                        let new_context_id = c.force_new_context();
-                        c.push(&args, new_context_id);
-
+                        c.push(&args);
                         args
                     }
                 };