Update for arguments being only terms (#47)

* Update for arguments being only terms

The main impact is that ProofArg is removed and everything is made more uniform
since arguments are only terms.

* format

* Remove test for parsing assignment arg since it is no longer relevant

* Simplifying building substitution when checking `forall_inst`

* remove unused error

Author: HanielB

carcara/src/ast/node.rs

@@ -218,7 +218,7 @@ pub struct StepNode {
     pub premises: Vec<Rc<ProofNode>>,
 
     /// The step arguments, given via the `:args` attribute.
-    pub args: Vec<ProofArg>,
+    pub args: Vec<Rc<Term>>,
 
     /// The local premises that this step discharges, given via the `:discharge` attribute.
     pub discharge: Vec<Rc<ProofNode>>,

carcara/src/ast/polyeq.rs

@@ -10,8 +10,7 @@
 use rug::Rational;
 
 use super::{
-    AnchorArg, BindingList, Constant, Operator, ProofArg, ProofCommand, ProofStep, Rc, Sort,
-    Subproof, Term,
+    AnchorArg, BindingList, Constant, Operator, ProofCommand, ProofStep, Rc, Sort, Subproof, Term,
 };
 use crate::utils::HashMapStack;
 use std::time::{Duration, Instant};
@@ -683,16 +682,6 @@ impl PolyeqComparable for AnchorArg {
     }
 }
 
-impl PolyeqComparable for ProofArg {
-    fn eq(comp: &mut Polyeq, a: &Self, b: &Self) -> bool {
-        match (a, b) {
-            (ProofArg::Term(a), ProofArg::Term(b)) => comp.eq(a, b),
-            (ProofArg::Assign(sa, ta), ProofArg::Assign(sb, tb)) => sa == sb && comp.eq(ta, tb),
-            _ => false,
-        }
-    }
-}
-
 impl PolyeqComparable for ProofCommand {
     fn eq(comp: &mut Polyeq, a: &Self, b: &Self) -> bool {
         match (a, b) {

carcara/src/ast/printer.rs

@@ -356,10 +356,10 @@ impl<'a> AlethePrinter<'a> {
 
         if let [head, tail @ ..] = step.args.as_slice() {
             write!(self.inner, " :args (")?;
-            self.write_proof_arg(head)?;
+            head.print_with_sharing(self)?;
             for arg in tail {
                 write!(self.inner, " ")?;
-                self.write_proof_arg(arg)?;
+                arg.print_with_sharing(self)?;
             }
             write!(self.inner, ")")?;
         }
@@ -378,17 +378,6 @@ impl<'a> AlethePrinter<'a> {
         Ok(())
     }
 
-    fn write_proof_arg(&mut self, arg: &ProofArg) -> io::Result<()> {
-        match arg {
-            ProofArg::Term(t) => t.print_with_sharing(self),
-            ProofArg::Assign(name, value) => {
-                write!(self.inner, "(:= {} ", name)?;
-                value.print_with_sharing(self)?;
-                write!(self.inner, ")")
-            }
-        }
-    }
-
     fn write_lia_smt_instance(&mut self, clause: &[Rc<Term>]) -> io::Result<()> {
         for term in clause.iter().dedup() {
             write!(self.inner, "(assert (not ")?;

carcara/src/ast/proof.rs

@@ -1,5 +1,4 @@
 use super::{ProofIter, Rc, SortedVar, Term};
-use crate::CheckerError;
 
 /// A proof in the Alethe format.
 #[derive(Debug, Clone)]
@@ -46,23 +45,13 @@ pub struct ProofStep {
     pub premises: Vec<(usize, usize)>,
 
     /// The step arguments, given via the `:args` attribute.
-    pub args: Vec<ProofArg>,
+    pub args: Vec<Rc<Term>>,
 
     /// The local premises that this step discharges, given via the `:discharge` attribute, and
     /// indexed similarly to premises.
     pub discharge: Vec<(usize, usize)>,
 }
 
-/// An argument for a `step` command.
-#[derive(Debug, Clone, PartialEq, Eq)]
-pub enum ProofArg {
-    /// An argument that is just a term.
-    Term(Rc<Term>),
-
-    /// An argument of the form `(:= <symbol> <term>)`.
-    Assign(String, Rc<Term>),
-}
-
 /// A subproof.
 ///
 /// Subproofs are started by `anchor` commands, and contain a series of steps, possibly including
@@ -141,26 +130,6 @@ impl ProofCommand {
     }
 }
 
-impl ProofArg {
-    /// If this argument is a "term style" argument, extracts that term from it. Otherwise, returns
-    /// an error.
-    pub fn as_term(&self) -> Result<&Rc<Term>, CheckerError> {
-        match self {
-            ProofArg::Term(t) => Ok(t),
-            ProofArg::Assign(s, t) => Err(CheckerError::ExpectedTermStyleArg(s.clone(), t.clone())),
-        }
-    }
-
-    /// If this argument is an "assign style" argument, extracts the variable name and the value
-    /// term from it. Otherwise, returns an error.
-    pub fn as_assign(&self) -> Result<(&String, &Rc<Term>), CheckerError> {
-        match self {
-            ProofArg::Assign(s, t) => Ok((s, t)),
-            ProofArg::Term(t) => Err(CheckerError::ExpectedAssignStyleArg(t.clone())),
-        }
-    }
-}
-
 impl AnchorArg {
     /// Returns `Some` if the anchor arg is a "variable" style argument.
     pub fn as_variable(&self) -> Option<&SortedVar> {

carcara/src/checker/error.rs

@@ -126,12 +126,6 @@ pub enum CheckerError {
     #[error("expected 'let' term, got '{0}'")]
     ExpectedLetTerm(Rc<Term>),
 
-    #[error("expected term style argument, got assign style argument: '(:= {0} {1})'")]
-    ExpectedTermStyleArg(String, Rc<Term>),
-
-    #[error("expected assign style '(:= ...)' argument, got term style argument: '{0}'")]
-    ExpectedAssignStyleArg(Rc<Term>),
-
     #[error("expected term {0} to be a prefix of {1}")]
     ExpectedToBePrefix(Rc<Term>, Rc<Term>),
 

carcara/src/checker/rules/linear_arithmetic.rs

@@ -263,7 +263,6 @@ pub fn la_generic(RuleArgs { conclusion, args, .. }: RuleArgs) -> RuleResult {
     let args: Vec<_> = args
         .iter()
         .map(|a| {
-            let a = a.as_term()?;
             a.as_fraction()
                 .ok_or_else(|| CheckerError::ExpectedAnyNumber(a.clone()))
         })

carcara/src/checker/rules/mod.rs

@@ -15,7 +15,7 @@ pub type Rule = fn(RuleArgs) -> RuleResult;
 pub struct RuleArgs<'a> {
     pub(super) conclusion: &'a [Rc<Term>],
     pub(super) premises: &'a [Premise<'a>],
-    pub(super) args: &'a [ProofArg],
+    pub(super) args: &'a [Rc<Term>],
     pub(super) pool: &'a mut dyn TermPool,
     pub(super) context: &'a mut ContextStack,
 
@@ -85,7 +85,7 @@ fn assert_clause_len<T: Into<Range>>(clause: &[Rc<Term>], range: T) -> RuleResul
     Ok(())
 }
 
-fn assert_num_args<T: Into<Range>>(args: &[ProofArg], range: T) -> RuleResult {
+fn assert_num_args<T: Into<Range>>(args: &[Rc<Term>], range: T) -> RuleResult {
     let range = range.into();
     if !range.contains(args.len()) {
         return Err(CheckerError::WrongNumberOfArgs(range, args.len()));

carcara/src/checker/rules/quantifier.rs

@@ -17,31 +17,18 @@ pub fn forall_inst(
 
     assert_num_args(args, bindings.len())?;
 
-    // Since the bindings and arguments may not be in the same order, we collect the bindings into
-    // a hash set, and remove each binding from it as we find the associated argument
-    let mut bindings: IndexSet<_> = bindings.iter().cloned().collect();
-    let substitution: IndexMap<_, _> = args
+    // iterate over the bindings and arguments simultaneously, building the substitution
+    let substitution: IndexMap<_, _> = bindings
         .iter()
-        .map(|arg| {
-            let (arg_name, arg_value) = arg.as_assign()?;
-            let arg_sort = pool.sort(arg_value);
-            rassert!(
-                bindings.remove(&(arg_name.clone(), arg_sort.clone())),
-                QuantifierError::NoBindingMatchesArg(arg_name.clone())
-            );
-
-            let ident_term = (arg_name.clone(), arg_sort).into();
-            Ok((pool.add(ident_term), arg_value.clone()))
+        .zip(args)
+        .map(|((var_name, sort), value)| {
+            assert_eq(sort, &pool.sort(value))?;
+            let var = pool.add(Term::new_var(var_name, sort.clone()));
+            Ok((var.clone(), value.clone()))
         })
         .collect::<Result<_, CheckerError>>()?;
     let mut substitution = Substitution::new(pool, substitution)?;
 
-    // All bindings were accounted for in the arguments
-    rassert!(
-        bindings.is_empty(),
-        QuantifierError::NoArgGivenForBinding(bindings.iter().next().unwrap().0.clone())
-    );
-
     // Equalities may be reordered, and the application of the substitution might rename bound
     // variables, so we need to compare for alpha-equivalence here
     let expected = substitution.apply(pool, original);
@@ -325,47 +312,47 @@ mod tests {
             ",
             "Simple working examples" {
                 "(step t1 (cl (or (not (forall ((p Bool)) p)) q))
-                    :rule forall_inst :args ((:= p q)))": true,
+                    :rule forall_inst :args (q))": true,
 
                 "(step t1 (cl (or (not (forall ((x Real) (y Real)) (= x y))) (= a b)))
-                    :rule forall_inst :args ((:= x a) (:= y b)))": true,
+                    :rule forall_inst :args (a b))": true,
 
                 "(step t1 (cl (or (not (forall ((x Real)) (= x a))) (= a a)))
-                    :rule forall_inst :args ((:= x a)))": true,
+                    :rule forall_inst :args (a))": true,
 
                 "(step t1 (cl (or (not (forall ((p Bool)) p)) (ite q (= a b) (and (= a 0.0) true))))
-                    :rule forall_inst :args ((:= p (ite q (= a b) (and (= a 0.0) true)))))": true,
+                    :rule forall_inst :args ((ite q (= a b) (and (= a 0.0) true))))": true,
             }
             "Equalities may be flipped" {
                 "(step t1 (cl (or (not (forall ((x Real) (y Real)) (and (= x y) (= 1 0))))
-                    (and (= b a) (= 1 0)))) :rule forall_inst :args ((:= x a) (:= y b)))": true,
+                    (and (= b a) (= 1 0)))) :rule forall_inst :args (a b))": true,
             }
             "Bound variables may be renamed by substitution" {
                 // The variable shadowing makes it so the substitution applied by Carcara renames p
                 "(step t1 (cl (or
                     (not (forall ((p Bool) (r Bool)) (and p (forall ((p Bool)) p))))
                     (and q (forall ((p Bool)) p))
-                )) :rule forall_inst :args ((:= p q) (:= r q)))": true,
+                )) :rule forall_inst :args (q q))": true,
             }
             "Argument is not in quantifier bindings" {
                 "(step t1 (cl (or (not (forall ((x Real)) (= x a))) (= b 0.0)))
-                    :rule forall_inst :args ((:= x b) (:= a 0.0)))": false,
+                    :rule forall_inst :args (b 0.0))": false,
             }
             "Binding has no associated substitution" {
                 "(step t1 (cl (or (not (forall ((x Real) (y Real)) (= x x))) (= a a)))
-                    :rule forall_inst :args ((:= x a)))": false,
+                    :rule forall_inst :args (a))": false,
             }
             "Substitution was not applied" {
                 "(step t1 (cl (or (not (forall ((x Real) (y Real)) (= x y))) (= x b)))
-                    :rule forall_inst :args ((:= x a) (:= y b)))": false,
+                    :rule forall_inst :args (a b))": false,
             }
             "Applied substitution was not passed as argument" {
                 "(step t1 (cl (or (not (forall ((x Real) (y Real)) (= x y))) (= a b)))
-                    :rule forall_inst :args ((:= x a)))": false,
+                    :rule forall_inst :args (a))": false,
             }
             "Wrong type of rule argument" {
                 "(step t1 (cl (or (not (forall ((x Real) (y Real)) (= x y))) (= a b)))
-                    :rule forall_inst :args ((:= x a) b))": false,
+                    :rule forall_inst :args ((= x a) b))": false,
             }
         }
     }

carcara/src/checker/rules/resolution.rs

@@ -132,7 +132,7 @@ pub fn strict_resolution(
 
 fn apply_generic_resolution<'a, C: ClauseCollection<'a>>(
     premises: &'a [Premise],
-    args: &'a [ProofArg],
+    args: &'a [Rc<Term>],
     pool: &mut dyn TermPool,
 ) -> Result<C, CheckerError> {
     assert_num_premises(premises, 2..)?;
@@ -142,8 +142,8 @@ fn apply_generic_resolution<'a, C: ClauseCollection<'a>>(
     let args: Vec<_> = args
         .chunks(2)
         .map(|chunk| {
-            let pivot = chunk[0].as_term()?.remove_all_negations();
-            let polarity = chunk[1].as_term()?;
+            let pivot = chunk[0].remove_all_negations();
+            let polarity = chunk[1].clone();
             let polarity = if polarity.is_bool_true() {
                 true
             } else if polarity.is_bool_false() {

carcara/src/checker/rules/strings.rs

@@ -340,7 +340,7 @@ pub fn concat_eq(
     match_term_err!((= x y) = &conclusion[0])?;
 
     let term = get_premise_term(&premises[0])?;
-    let rev = args[0].as_term()?.as_bool_err()?;
+    let rev = args[0].as_bool_err()?;
     let (s, t) = match_term_err!((= s t) = term)?;
 
     let (ss, ts) = strip_prefix_or_suffix(pool, s.clone(), t.clone(), rev, polyeq_time)?;
@@ -374,7 +374,7 @@ pub fn concat_unify(
 
     let term = get_premise_term(&premises[0])?;
     let prefixes = get_premise_term(&premises[1])?;
-    let rev = args[0].as_term()?.as_bool_err()?;
+    let rev = args[0].as_bool_err()?;
     let (s, t) = match_term_err!((= s t) = term)?;
     let (s_1, t_1) = match_term_err!((= (strlen s_1) (strlen t_1)) = prefixes)?;
 
@@ -407,7 +407,7 @@ pub fn concat_conflict(
     assert_clause_len(conclusion, 1)?;
 
     let term = get_premise_term(&premises[0])?;
-    let rev = args[0].as_term()?.as_bool_err()?;
+    let rev = args[0].as_bool_err()?;
     if conclusion[0].as_bool_err()? {
         return Err(CheckerError::ExpectedBoolConstant(
             false,
@@ -890,7 +890,7 @@ pub fn string_decompose(
     assert_clause_len(conclusion, 1)?;
 
     let term = get_premise_term(&premises[0])?;
-    let rev = args[0].as_term()?.as_bool_err()?;
+    let rev = args[0].as_bool_err()?;
     let (t, n) = match_term_err!((>= (strlen t) n) = term)?;
 
     match_term_err!(
@@ -919,7 +919,7 @@ pub fn string_length_pos(RuleArgs { args, conclusion, polyeq_time, .. }: RuleArg
     assert_num_args(args, 1)?;
     assert_clause_len(conclusion, 1)?;
 
-    let t = args[0].as_term()?;
+    let t = &args[0];
     let (((t_1, _), (t_2, _)), (t_3, _)) = match_term_err!(
         (or
             (and

carcara/src/elaborator/mod.rs

@@ -223,10 +223,7 @@ impl<'e> Elaborator<'e> {
             clause: vec![term.clone()],
             rule: "resolution".to_owned(),
             premises: vec![new_assume, equiv1_step],
-            args: vec![
-                ProofArg::Term(premise),
-                ProofArg::Term(self.pool.bool_true()),
-            ],
+            args: vec![premise, self.pool.bool_true()],
             ..Default::default()
         }))
     }

carcara/src/elaborator/reordering.rs

@@ -63,8 +63,8 @@ fn recompute_resolution(step: &StepNode) -> Vec<Rc<Term>> {
         .args
         .chunks(2)
         .map(|chunk| {
-            let pivot = chunk[0].as_term().unwrap();
-            let polarity = chunk[1].as_term().unwrap().is_bool_true();
+            let pivot = &chunk[0];
+            let polarity = chunk[1].is_bool_true();
             (pivot, polarity)
         })
         .collect();

carcara/src/elaborator/resolution.rs

@@ -27,9 +27,7 @@ pub fn resolution(
                     clause: Vec::new(),
                     rule: "resolution".to_owned(),
                     premises: vec![step.premises[0].clone(), true_step],
-                    args: [true, false]
-                        .map(|a| ProofArg::Term(pool.bool_constant(a)))
-                        .to_vec(),
+                    args: [true, false].map(|a| pool.bool_constant(a)).to_vec(),
                     ..Default::default()
                 })));
             }
@@ -62,7 +60,6 @@ pub fn resolution(
     let pivots = pivot_trace
         .into_iter()
         .flat_map(|(pivot, polarity)| [pivot, pool.bool_constant(polarity)])
-        .map(ProofArg::Term)
         .collect();
 
     let mut resolution_step = StepNode {
@@ -128,7 +125,6 @@ pub fn resolution(
         // original resolution step's conclusion
         let args = [c, pool.bool_true(), quadruple_not_c, pool.bool_true()]
             .into_iter()
-            .map(ProofArg::Term)
             .collect();
 
         Ok(Rc::new(ProofNode::Step(StepNode {

carcara/src/elaborator/transitivity.rs

@@ -267,7 +267,6 @@ fn flip_eq_transitive_premises(
     let args: Vec<_> = resolution_pivots
         .into_iter()
         .flat_map(|(_, pivot, _)| [pivot, pool.bool_false()])
-        .map(ProofArg::Term)
         .collect();
 
     Rc::new(ProofNode::Step(StepNode {