Replace remaining or_intros with weakening

ufmg-smite · Aug 13, 2024 · f3bb55d · f3bb55d
1 parent e517c02
commit f3bb55d
Show file tree

Hide file tree

Showing 3 changed files with 6 additions and 6 deletions.
diff --git 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
@@ -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
@@ -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;