From f3bb55d22762a0bb04c13b46de3e64136cf34b7d Mon Sep 17 00:00:00 2001
From: Bruno Andreotti <bandreotti@proton.me>
Date: Tue, 13 Aug 2024 14:29:22 -0300
Subject: [PATCH] Replace remaining `or_intro`s with `weakening`

---
 carcara/src/elaborator/reordering.rs   | 4 ++--
 carcara/src/elaborator/transitivity.rs | 2 +-
 carcara/src/elaborator/uncrowding.rs   | 6 +++---
 3 files changed, 6 insertions(+), 6 deletions(-)

diff --git a/carcara/src/elaborator/reordering.rs b/carcara/src/elaborator/reordering.rs
index fa4cdd88..5c472a04 100644
--- a/carcara/src/elaborator/reordering.rs
+++ b/carcara/src/elaborator/reordering.rs
@@ -37,14 +37,14 @@ type RecomputationFunc = fn(&StepNode) -> Vec<Rc<Term>>;
 
 fn get_recomputation_func(rule: &str) -> Option<RecomputationFunc> {
     Some(match rule {
-        "or_intro" => recompute_or_intro,
+        "weakening" => recompute_weakening,
         "contraction" => recompute_contraction,
         "resolution" | "th_resolution" | "strict_resolution" => recompute_resolution,
         _ => return None,
     })
 }
 
-fn recompute_or_intro(step: &StepNode) -> Vec<Rc<Term>> {
+fn recompute_weakening(step: &StepNode) -> Vec<Rc<Term>> {
     let mut new = step.clause.clone();
     let premise = step.premises[0].clause();
     new[..premise.len()].clone_from_slice(premise);
diff --git a/carcara/src/elaborator/transitivity.rs b/carcara/src/elaborator/transitivity.rs
index 10cd5a1d..dcde5bce 100644
--- a/carcara/src/elaborator/transitivity.rs
+++ b/carcara/src/elaborator/transitivity.rs
@@ -184,7 +184,7 @@ pub fn eq_transitive(
             id: ids.next_id(),
             depth: step.depth,
             clause,
-            rule: "or_intro".to_owned(),
+            rule: "weakening".to_owned(),
             premises: vec![latest_step],
             args: Vec::new(),
             discharge: Vec::new(),
diff --git a/carcara/src/elaborator/uncrowding.rs b/carcara/src/elaborator/uncrowding.rs
index e08cc6de..cf445967 100644
--- a/carcara/src/elaborator/uncrowding.rs
+++ b/carcara/src/elaborator/uncrowding.rs
@@ -106,12 +106,12 @@ pub fn uncrowd_resolution(
     let mut final_step = premises[previous_cut].node.as_step().unwrap().clone();
 
     if final_step.clause.len() != step.clause.len() {
-        let clause = get_or_intro_clause(&final_step.clause, &step.clause);
+        let clause = get_weakening_clause(&final_step.clause, &step.clause);
         final_step = StepNode {
             id: ids.next_id(),
             depth: step.depth,
             clause,
-            rule: "or_intro".to_owned(),
+            rule: "weakening".to_owned(),
             premises: vec![Rc::new(ProofNode::Step(final_step))],
             ..Default::default()
         }
@@ -190,7 +190,7 @@ fn add_partial_resolution_step<'a>(
     }
 }
 
-fn get_or_intro_clause(current: &[Rc<Term>], target: &[Rc<Term>]) -> Vec<Rc<Term>> {
+fn get_weakening_clause(current: &[Rc<Term>], target: &[Rc<Term>]) -> Vec<Rc<Term>> {
     let mut missing: HashMap<&Rc<Term>, usize> = HashMap::new();
     for term in target {
         *missing.entry(term).or_default() += 1;