wip

carcara/src/ast/context.rs

@@ -1,42 +1,17 @@
 use crate::ast::*;
 use std::sync::{atomic::AtomicUsize, Arc, RwLock, RwLockReadGuard, RwLockWriteGuard};
 
+#[derive(Debug)]
 pub struct Context {
-    pub mappings: Vec<(Rc<Term>, Rc<Term>)>,
-    pub bindings: IndexSet<SortedVar>,
+    pub args: Vec<AnchorArg>,
     pub cumulative_substitution: Option<Substitution>,
 }
 
 impl Context {
     /// Builds a new context form the arguments to an `anchor`. This does not initalize the
     /// `cumulative_substitution` field.
-    fn build(
-        pool: &mut dyn TermPool,
-        assignment_args: &[(String, Rc<Term>)],
-        variable_args: &[SortedVar],
-    ) -> Result<Self, SubstitutionError> {
-        // We build the context mappings incrementally, using the mappings already
-        // introduced to transform the result of a new mapping before adding it. So for
-        // instance, if the mappings are `(:= y z)` and `(:= x (f y))`, we insert the first
-        // mapping, and then, when introducing the second, we use the current state of the
-        // substitutions to transform `(f y)` into `(f z)`. The resulting mappings will then
-        // contain `(:= y z)` and `(:= x (f z))`
-        let mut substitution = Substitution::empty();
-        let mappings = assignment_args
-            .iter()
-            .map(|(var, value)| {
-                let var_term = pool.add(Term::new_var(var, pool.sort(value)));
-                let new_value = substitution.apply(pool, value);
-                substitution.insert(pool, var_term.clone(), new_value.clone())?;
-                Ok((var_term, new_value))
-            })
-            .collect::<Result<_, _>>()?;
-
-        Ok(Self {
-            mappings,
-            bindings: variable_args.iter().cloned().collect(),
-            cumulative_substitution: None,
-        })
+    fn new(args: Vec<AnchorArg>) -> Self {
+        Self { args, cumulative_substitution: None }
     }
 }
 
@@ -47,7 +22,7 @@ impl Context {
 /// `1`: Shareable and droppable slot for the context.
 type ContextInfo = (AtomicUsize, RwLock<Option<Context>>);
 
-#[derive(Default)]
+#[derive(Default, Debug)]
 /// Struct that implements a thread-shared context stack. That way, this stack
 /// tries to use an already existing global `Context` (built by another thread).
 /// If it was still not built, then the current thread is going to build this
@@ -127,19 +102,13 @@ impl ContextStack {
         ctx_vec.len() - 1
     }
 
-    pub fn push(
-        &mut self,
-        pool: &mut dyn TermPool,
-        assignment_args: &[(String, Rc<Term>)],
-        variable_args: &[SortedVar],
-        context_id: usize,
-    ) -> Result<(), SubstitutionError> {
+    pub fn push(&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
             // build this context at the context vec (accessible for all threads)
             if ctx_write_guard.is_none() {
-                *ctx_write_guard = Some(Context::build(pool, assignment_args, variable_args)?);
+                *ctx_write_guard = Some(Context::new(args.to_vec()));
             }
         }
         // Adds this context in the stack
@@ -148,7 +117,6 @@ impl ContextStack {
         // required at any moment, then we are assured it will wait until the
         // fully context construction
         self.stack.push(context_id);
-        Ok(())
     }
 
     pub fn pop(&mut self) {
@@ -180,12 +148,9 @@ impl ContextStack {
             // necessary, we require the write guard. This tries to avoid bigger
             // overheads
             let context_guard = self.context_vec[self.stack[i]].1.read().unwrap();
-            let curr_context = context_guard.as_ref().unwrap();
-
-            let simultaneous = build_simultaneous_substitution(pool, &curr_context.mappings).map;
-            let mut cumulative_substitution = simultaneous.clone();
+            let current_context = context_guard.as_ref().unwrap();
 
-            if i > 0 {
+            let mut substitution = if i > 0 {
                 // Waits until OS allows to read this previous context. The code structure
                 // makes sure that this context, when released for reading, will be already
                 // instantiated since there are only 2 cases:
@@ -194,31 +159,39 @@ impl ContextStack {
                 //  - Another thread was assigned to build this context. Then, it doesn't
                 //      matter if this other thread has already finished the process, the
                 //      current thread will have to wait until the guard is released.
-                if let Some(previous_context) = self
-                    .stack
-                    .get(i - 1)
-                    .map(|id| self.context_vec[*id].1.read().unwrap())
-                {
-                    let previous_context = previous_context.as_ref().unwrap();
-                    let previous_substitution =
-                        previous_context.cumulative_substitution.as_ref().unwrap();
+                let guard = self.context_vec[self.stack[i - 1]].1.read().unwrap();
+                guard
+                    .as_ref()
+                    .unwrap()
+                    .cumulative_substitution
+                    .clone()
+                    .unwrap()
+            } else {
+                Substitution::empty()
+            };
 
-                    for (k, v) in &previous_substitution.map {
-                        let value = match simultaneous.get(v) {
-                            Some(new_value) => new_value,
-                            None => v,
-                        };
-                        cumulative_substitution.insert(k.clone(), value.clone());
+            for a in &current_context.args {
+                match a {
+                    AnchorArg::Variable((name, sort)) => {
+                        let var_term = pool.add(Term::new_var(name, sort.clone()));
+                        substitution.remove(&var_term);
+                    }
+                    AnchorArg::Assign(name, value) => {
+                        let var_term = pool.add(Term::new_var(name, pool.sort(value)));
+                        let new_value = substitution.apply(pool, value);
+                        // It is safe to unwrap here because we ensure by contruction that
+                        // `var_term` is a variable term, with he same sort as `value`
+                        substitution
+                            .insert(pool, var_term, new_value.clone())
+                            .unwrap();
                     }
                 }
             }
-            drop(context_guard);
 
-            // Waits until the OS allows to mutate at this context
-            // TODO: Does it really needs to require a write guard here instead of up there
+            // Drop the read guard, and acquire a write guard
+            drop(context_guard);
             let mut context_guard = self.context_vec[self.stack[i]].1.write().unwrap();
-            context_guard.as_mut().unwrap().cumulative_substitution =
-                Some(Substitution::new(pool, cumulative_substitution).unwrap());
+            context_guard.as_mut().unwrap().cumulative_substitution = Some(substitution);
             self.num_cumulative_calculated = i + 1;
         }
     }

carcara/src/ast/mod.rs

@@ -155,13 +155,13 @@ pub struct Subproof {
     /// The proof commands inside the subproof.
     pub commands: Vec<ProofCommand>,
 
-    /// The "assignment" style arguments of the subproof, of the form `(:= <symbol> <term>)`.
-    pub assignment_args: Vec<(String, Rc<Term>)>,
-
-    /// The "variable" style arguments of the subproof, of the form `(<symbol> <sort>)`.
-    pub variable_args: Vec<SortedVar>,
+    /// The arguments of the subproof.
+    ///
+    /// They can be either a variable declaration, of the form `(<symbol> <sort>)`, or an
+    /// assignment, of the form `(:= <symbol> <term>)`.
+    pub args: Vec<AnchorArg>,
 
-    /// Subproof id used for context hashing purpose
+    /// Subproof id used for context hashing purposes.
     pub context_id: usize,
 }
 
@@ -195,6 +195,16 @@ impl ProofArg {
     }
 }
 
+/// An argument for an `anchor` command.
+#[derive(Debug, Clone, PartialEq)]
+pub enum AnchorArg {
+    /// A "variable declaration" style argument, of the form `(<symbol> <sort>)`.
+    Variable(SortedVar),
+
+    /// An "assignment" style argument, of the form `(:= <symbol> <term>)`.
+    Assign(String, Rc<Term>),
+}
+
 /// The operator of an operation term.
 #[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
 pub enum Operator {

carcara/src/ast/polyeq.rs

@@ -7,7 +7,9 @@
 //! - `alpha_equiv` compares terms by alpha-equivalence, meaning it implements equality of terms
 //! modulo renaming of bound variables.
 
-use super::{BindingList, Operator, ProofArg, ProofCommand, ProofStep, Rc, Sort, Subproof, Term};
+use super::{
+    AnchorArg, BindingList, Operator, ProofArg, ProofCommand, ProofStep, Rc, Sort, Subproof, Term,
+};
 use crate::utils::HashMapStack;
 use std::time::{Duration, Instant};
 
@@ -402,6 +404,18 @@ impl Polyeq for String {
     }
 }
 
+impl Polyeq for AnchorArg {
+    fn eq(comp: &mut PolyeqComparator, a: &Self, b: &Self) -> bool {
+        match (a, b) {
+            (AnchorArg::Variable(a), AnchorArg::Variable(b)) => Polyeq::eq(comp, a, b),
+            (AnchorArg::Assign(a_name, a_value), AnchorArg::Assign(b_name, b_value)) => {
+                a_name == b_name && Polyeq::eq(comp, a_value, b_value)
+            }
+            _ => false,
+        }
+    }
+}
+
 impl Polyeq for ProofArg {
     fn eq(comp: &mut PolyeqComparator, a: &Self, b: &Self) -> bool {
         match (a, b) {
@@ -441,9 +455,7 @@ impl Polyeq for ProofStep {
 
 impl Polyeq for Subproof {
     fn eq(comp: &mut PolyeqComparator, a: &Self, b: &Self) -> bool {
-        Polyeq::eq(comp, &a.commands, &b.commands)
-            && Polyeq::eq(comp, &a.assignment_args, &b.assignment_args)
-            && Polyeq::eq(comp, &a.variable_args, &b.variable_args)
+        Polyeq::eq(comp, &a.commands, &b.commands) && Polyeq::eq(comp, &a.args, &b.args)
     }
 }
 

carcara/src/ast/printer.rs

@@ -143,27 +143,31 @@ impl<'a> PrintProof for AlethePrinter<'a> {
                 ProofCommand::Subproof(s) => {
                     write!(self.inner, "(anchor :step {}", quote_symbol(command.id()))?;
 
-                    if !s.variable_args.is_empty() || !s.assignment_args.is_empty() {
+                    if !s.args.is_empty() {
                         write!(self.inner, " :args (")?;
                         let mut is_first = true;
-                        for var in &s.variable_args {
+                        for arg in &s.args {
                             if !is_first {
                                 write!(self.inner, " ")?;
+                                is_first = false;
                             }
-                            is_first = false;
-                            var.print_with_sharing(self)?;
-                        }
-                        for (name, value) in &s.assignment_args {
-                            if !is_first {
-                                write!(self.inner, " ")?;
+
+                            match arg {
+                                AnchorArg::Variable((name, sort)) => {
+                                    write!(self.inner, "({} ", quote_symbol(name))?;
+                                    sort.print_with_sharing(self)?;
+                                    write!(self.inner, ")")?;
+                                }
+                                AnchorArg::Assign(name, value) => {
+                                    write!(self.inner, "(:= {} ", name)?;
+                                    value.print_with_sharing(self)?;
+                                    write!(self.inner, ")")?;
+                                }
                             }
-                            is_first = false;
-                            write!(self.inner, "(:= {} ", name)?;
-                            value.print_with_sharing(self)?;
-                            write!(self.inner, ")")?;
                         }
                         write!(self.inner, ")")?;
                     }
+
                     write!(self.inner, ")")?;
                 }
             }

carcara/src/ast/substitution.rs

@@ -34,9 +34,10 @@ type SubstitutionResult<T> = Result<T, SubstitutionError>;
 /// substitutions are also capture-avoiding. This is done by renaming the binder variable when
 /// necessary before applying the substitution. In the earlier example, the resulting term would
 /// actually be `(forall ((y' Int)) (= y y'))`.
+#[derive(Debug, Clone)]
 pub struct Substitution {
     /// The substitution's mappings.
-    pub(crate) map: IndexMap<Rc<Term>, Rc<Term>>,
+    pub(super) map: IndexMap<Rc<Term>, Rc<Term>>,
 
     /// The variables that should be renamed to preserve capture-avoidance, if they are bound by a
     /// binder term.
@@ -123,6 +124,17 @@ impl Substitution {
         Ok(())
     }
 
+    /// Removes a mapping from the substitution.
+    ///
+    /// This will clear `self.should_be_renamed`, such that it might need to be recomputed later.
+    /// Therefore, you should avoid using this method if possible.
+    pub(super) fn remove(&mut self, x: &Rc<Term>) {
+        let was_present = self.map.remove(x).is_some();
+        if was_present {
+            self.should_be_renamed = None;
+        }
+    }
+
     /// Computes which binder variables will need to be renamed, and stores the result in
     /// `self.should_be_renamed`.
     fn compute_should_be_renamed(&mut self, pool: &mut dyn TermPool) {

carcara/src/checker/lia_generic.rs

@@ -227,7 +227,6 @@ fn insert_solver_proof(
     }
 
     let subproof = elaborator.close_accumulator_subproof(
-        Vec::new(),
         Vec::new(),
         ProofStep {
             id: subproof_id,

carcara/src/checker/mod.rs

@@ -161,18 +161,7 @@ impl<'c> ProofChecker<'c> {
                     let step_id = command.id();
 
                     let new_context_id = self.context.force_new_context();
-                    self.context
-                        .push(
-                            self.pool,
-                            &s.assignment_args,
-                            &s.variable_args,
-                            new_context_id,
-                        )
-                        .map_err(|e| Error::Checker {
-                            inner: e.into(),
-                            rule: "anchor".into(),
-                            step: step_id.to_owned(),
-                        })?;
+                    self.context.push(&s.args, new_context_id);
 
                     if let Some(elaborator) = &mut self.elaborator {
                         elaborator.open_subproof(s.commands.len());

carcara/src/checker/parallel/mod.rs

@@ -287,22 +287,17 @@ impl<'c> ParallelProofChecker<'c> {
                     let time = Instant::now();
                     let step_id = command.id();
 
-                    self.context
-                        .push(
-                            &mut pool.ctx_pool,
-                            &s.assignment_args,
-                            &s.variable_args,
-                            s.context_id,
-                        )
-                        .map_err(|e| {
-                            // Signalize to other threads to stop the proof checking
-                            should_abort.store(true, Ordering::Release);
-                            Error::Checker {
-                                inner: e.into(),
-                                rule: "anchor".into(),
-                                step: step_id.to_owned(),
-                            }
-                        })?;
+                    self.context.push(&s.args, s.context_id);
+                    // TODO
+                    // .map_err(|e| {
+                    //     // Signalize to other threads to stop the proof checking
+                    //     should_abort.store(true, Ordering::Release);
+                    //     Error::Checker {
+                    //         inner: e.into(),
+                    //         rule: "anchor".into(),
+                    //         step: step_id.to_owned(),
+                    //     }
+                    // })?;
 
                     if let Some(stats) = &mut stats {
                         // Collects statistics

carcara/src/checker/rules/reflexivity.rs

@@ -36,6 +36,7 @@ pub fn refl(
     // don't compute the new left and right terms until they are needed, to avoid doing unnecessary
     // work
     let new_left = context.apply(pool, left);
+    // dbg!(&context);
     let result = alpha_equiv(&new_left, right, polyeq_time) || {
         let new_right = context.apply(pool, right);
         alpha_equiv(left, &new_right, polyeq_time)