Don't store duplicate outbound premises

ufmg-smite · May 16, 2024 · f031c82 · f031c82
1 parent 1e491e3
commit f031c82
Showing 1 changed file with 6 additions and 6 deletions.
diff --git a/carcara/src/ast/node.rs b/carcara/src/ast/node.rs
@@ -128,14 +128,14 @@ pub fn proof_list_to_node(commands: Vec<ProofCommand>) -> Rc<ProofNode> {
         commands: std::vec::IntoIter<ProofCommand>,
         accumulator: Vec<Rc<ProofNode>>,
         args: Vec<AnchorArg>,
-        outbound_premises: Vec<Rc<ProofNode>>,
+        outbound_premises: IndexSet<Rc<ProofNode>>,
     }
 
     let mut stack: Vec<Frame> = vec![Frame {
         commands: commands.into_iter(),
         accumulator: Vec::new(),
         args: Vec::new(),
-        outbound_premises: Vec::new(),
+        outbound_premises: IndexSet::new(),
     }];
 
     let new_root_proof = loop {
@@ -159,7 +159,7 @@ pub fn proof_list_to_node(commands: Vec<ProofCommand>) -> Rc<ProofNode> {
                 for p in &premises {
                     if p.depth() < stack.len() - 1 {
                         let frame = stack.last_mut().unwrap();
-                        frame.outbound_premises.push(p.clone());
+                        frame.outbound_premises.insert(p.clone());
                     }
                 }
 
@@ -186,7 +186,7 @@ pub fn proof_list_to_node(commands: Vec<ProofCommand>) -> Rc<ProofNode> {
                     commands: s.commands.into_iter(),
                     accumulator: Vec::new(),
                     args: s.args,
-                    outbound_premises: Vec::new(),
+                    outbound_premises: IndexSet::new(),
                 };
                 stack.push(frame);
                 continue;
@@ -202,14 +202,14 @@ pub fn proof_list_to_node(commands: Vec<ProofCommand>) -> Rc<ProofNode> {
                 for p in &frame.outbound_premises {
                     if p.depth() < stack.len() - 1 {
                         let frame = stack.last_mut().unwrap();
-                        frame.outbound_premises.push(p.clone());
+                        frame.outbound_premises.insert(p.clone());
                     }
                 }
 
                 ProofNode::Subproof(SubproofNode {
                     last_step: frame.accumulator.pop().unwrap(),
                     args: frame.args,
-                    outbound_premises: frame.outbound_premises,
+                    outbound_premises: frame.outbound_premises.into_iter().collect(),
                 })
             }
         };