Skip to content

Commit

Permalink
Refactor elaborator module
Browse files Browse the repository at this point in the history
  • Loading branch information
@bpandreotti
bpandreotti committed Jun 3, 2024
1 parent 0a2f0f2 commit f380239
Show file tree
Hide file tree
Showing 5 changed files with 150 additions and 159 deletions.
21 changes: 11 additions & 10 deletions carcara/src/elaborator/lia_generic.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -54,23 +54,24 @@ fn get_problem_string(conclusion: &[Rc<Term>], prelude: &ProblemPrelude) -> Stri
problem
}

pub fn lia_generic(
pool: &mut PrimitivePool,
step: &StepNode,
prelude: &ProblemPrelude,
options: &LiaGenericOptions,
) -> Option<Rc<ProofNode>> {
let problem = get_problem_string(&step.clause, prelude);
let commands = match get_solver_proof(pool, problem, options) {
pub fn lia_generic(elaborator: &mut Elaborator, step: &StepNode) -> Option<Rc<ProofNode>> {
let problem = get_problem_string(&step.clause, elaborator.prelude);
let options = elaborator.config.lia_options.as_ref().unwrap();
let commands = match get_solver_proof(elaborator.pool, problem, options) {
Ok(c) => c,
Err(e) => {
log::warn!("failed to elaborate `lia_generic` step: {}", e);
return None;
}
};

let elaborated = insert_solver_proof(pool, commands, &step.clause, &step.id, step.depth);
Some(elaborated)
Some(insert_solver_proof(
elaborator.pool,
commands,
&step.clause,
&step.id,
step.depth,
))
}

fn get_solver_proof(
Expand Down
245 changes: 128 additions & 117 deletions carcara/src/elaborator/mod.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -55,138 +55,149 @@ pub struct LiaGenericOptions {
pub arguments: Vec<Box<str>>,
}

pub fn default_pipeline() -> Vec<ElaborationStep> {
use ElaborationStep::*;
vec![Polyeq, LiaGeneric, Local, Uncrowd, Reordering]
pub struct Elaborator<'e> {
pool: &'e mut PrimitivePool,
premises: &'e IndexSet<Rc<Term>>,
prelude: &'e ProblemPrelude,
config: Config,
}

pub fn elaborate(
pool: &mut PrimitivePool,
premises: &IndexSet<Rc<Term>>,
prelude: &ProblemPrelude,
root: &Rc<ProofNode>,
config: Config,
pipeline: Vec<ElaborationStep>,
) -> Rc<ProofNode> {
let mut current = root.clone();
for step in pipeline {
current = match step {
ElaborationStep::Polyeq => elaborate_polyeq(pool, premises, &current),
ElaborationStep::LiaGeneric => mutate(&current, |_, node| match node.as_ref() {
ProofNode::Step(s) if s.rule == "lia_generic" => {
lia_generic::lia_generic(pool, s, prelude, config.lia_options.as_ref().unwrap())
.unwrap_or_else(|| node.clone())
}
_ => node.clone(),
}),
ElaborationStep::Local => elaborate_local(pool, &current),
ElaborationStep::Uncrowd => mutate(&current, |_, node| match node.as_ref() {
ProofNode::Step(s)
if (s.rule == "resolution" || s.rule == "th_resolution")
&& !s.args.is_empty() =>
impl<'e> Elaborator<'e> {
pub fn new(
pool: &'e mut PrimitivePool,
premises: &'e IndexSet<Rc<Term>>,
prelude: &'e ProblemPrelude,
config: Config,
) -> Self {
Self { pool, premises, prelude, config }
}

pub fn elaborate_with_default_pipeline(&mut self, root: &Rc<ProofNode>) -> Rc<ProofNode> {
use ElaborationStep::*;
let pipeline = vec![Polyeq, LiaGeneric, Local, Uncrowd, Reordering];
self.elaborate(root, pipeline)
}

pub fn elaborate(
&mut self,
root: &Rc<ProofNode>,
pipeline: Vec<ElaborationStep>,
) -> Rc<ProofNode> {
let mut current = root.clone();
for step in pipeline {
current = match step {
ElaborationStep::Polyeq => self.elaborate_polyeq(&current),
ElaborationStep::LiaGeneric => mutate(&current, |_, node| match node.as_ref() {
ProofNode::Step(s) if s.rule == "lia_generic" => {
lia_generic::lia_generic(self, s).unwrap_or_else(|| node.clone())
}
_ => node.clone(),
}),
ElaborationStep::Local => self.elaborate_local(&current),
ElaborationStep::Uncrowd => mutate(&current, |_, node| match node.as_ref() {
ProofNode::Step(s)
if (s.rule == "resolution" || s.rule == "th_resolution")
&& !s.args.is_empty() =>
{
uncrowding::uncrowd_resolution(self.pool, s)
}
_ => node.clone(),
}),
ElaborationStep::Reordering => reordering::remove_reorderings(&current),
};
}
current
}

fn elaborate_polyeq(&mut self, root: &Rc<ProofNode>) -> Rc<ProofNode> {
mutate(root, |context, node| {
match node.as_ref() {
ProofNode::Assume { id, depth, term }
if context.is_empty() && !self.premises.contains(term) =>
{
uncrowding::uncrowd_resolution(pool, s)
self.elaborate_assume(id, *depth, term)
}
ProofNode::Step(s) if s.rule == "refl" => {
reflexivity::refl(self.pool, context, s).unwrap() // TODO: add proper error handling
}
_ => node.clone(),
}),
ElaborationStep::Reordering => reordering::remove_reorderings(&current),
};
}
})
}
current
}

fn elaborate_polyeq(
pool: &mut PrimitivePool,
premises: &IndexSet<Rc<Term>>,
root: &Rc<ProofNode>,
) -> Rc<ProofNode> {
mutate(root, |context, node| {
match node.as_ref() {
ProofNode::Assume { id, depth, term }
if context.is_empty() && !premises.contains(term) =>
{
elaborate_assume(pool, premises, id, *depth, term)
}
ProofNode::Step(s) if s.rule == "refl" => {
reflexivity::refl(pool, context, s).unwrap() // TODO: add proper error handling
}
_ => node.clone(),
fn elaborate_local(&mut self, root: &Rc<ProofNode>) -> Rc<ProofNode> {
fn get_elaboration_function(rule: &str) -> Option<ElaborationFunc> {
Some(match rule {
"eq_transitive" => transitivity::eq_transitive,
"trans" => transitivity::trans,
"resolution" | "th_resolution" => resolution::resolution,
_ => return None,
})
}
})
}

fn elaborate_local(pool: &mut PrimitivePool, root: &Rc<ProofNode>) -> Rc<ProofNode> {
fn get_elaboration_function(rule: &str) -> Option<ElaborationFunc> {
Some(match rule {
"eq_transitive" => transitivity::eq_transitive,
"trans" => transitivity::trans,
"resolution" | "th_resolution" => resolution::resolution,
_ => return None,
mutate(root, |context, node| {
match node.as_ref() {
ProofNode::Step(s) => {
if let Some(func) = get_elaboration_function(&s.rule) {
return func(self.pool, context, s).unwrap(); // TODO: add proper error handling
}
}
ProofNode::Subproof(_) => unreachable!(),
ProofNode::Assume { .. } => (),
}
node.clone()
})
}

mutate(root, |context, node| {
match node.as_ref() {
ProofNode::Step(s) => {
if let Some(func) = get_elaboration_function(&s.rule) {
return func(pool, context, s).unwrap(); // TODO: add proper error handling
}
fn elaborate_assume(&mut self, id: &str, depth: usize, term: &Rc<Term>) -> Rc<ProofNode> {
let mut found = None;
let mut polyeq_time = std::time::Duration::ZERO;
for p in self.premises {
if polyeq_mod_nary(term, p, &mut polyeq_time) {
found = Some(p.clone());
break;
}
ProofNode::Subproof(_) => unreachable!(),
ProofNode::Assume { .. } => (),
}
node.clone()
})
}

fn elaborate_assume(
pool: &mut dyn TermPool,
premises: &IndexSet<Rc<Term>>,
id: &str,
depth: usize,
term: &Rc<Term>,
) -> Rc<ProofNode> {
let mut found = None;
let mut polyeq_time = std::time::Duration::ZERO;
for p in premises {
if polyeq_mod_nary(term, p, &mut polyeq_time) {
found = Some(p.clone());
break;
}
let premise = found.expect("trying to elaborate assume, but it is invalid!");

let new_assume = Rc::new(ProofNode::Assume {
id: id.to_owned(),
depth,
term: premise.clone(),
});

let mut ids = IdHelper::new(id);
let equality_step = PolyeqElaborator::new(&mut ids, depth, false).elaborate(
self.pool,
premise.clone(),
term.clone(),
);

let equiv1_step = Rc::new(ProofNode::Step(StepNode {
id: ids.next_id(),
depth,
clause: vec![
build_term!(self.pool, (not {premise.clone()})),
term.clone(),
],
rule: "equiv1".to_owned(),
premises: vec![equality_step],
..Default::default()
}));

Rc::new(ProofNode::Step(StepNode {
id: ids.next_id(),
depth,
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()),
],
..Default::default()
}))
}
let premise = found.expect("trying to elaborate assume, but it is invalid!");

let new_assume = Rc::new(ProofNode::Assume {
id: id.to_owned(),
depth,
term: premise.clone(),
});

let mut ids = IdHelper::new(id);
let equality_step = PolyeqElaborator::new(&mut ids, depth, false).elaborate(
pool,
premise.clone(),
term.clone(),
);

let equiv1_step = Rc::new(ProofNode::Step(StepNode {
id: ids.next_id(),
depth,
clause: vec![build_term!(pool, (not {premise.clone()})), term.clone()],
rule: "equiv1".to_owned(),
premises: vec![equality_step],
..Default::default()
}));

Rc::new(ProofNode::Step(StepNode {
id: ids.next_id(),
depth,
clause: vec![term.clone()],
rule: "resolution".to_owned(),
premises: vec![new_assume, equiv1_step],
args: vec![ProofArg::Term(premise), ProofArg::Term(pool.bool_true())],
..Default::default()
}))
}

pub fn add_refl_step(
Expand Down
11 changes: 3 additions & 8 deletions carcara/src/lib.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -244,14 +244,9 @@ pub fn check_and_elaborate<T: io::BufRead>(
let elaboration = Instant::now();

let node = ast::ProofNode::from_commands(proof.commands);
let elaborated = elaborator::elaborate(
&mut pool,
&proof.premises,
&prelude,
&node,
elaborator_config,
elaborator::default_pipeline(),
);
let elaborated =
elaborator::Elaborator::new(&mut pool, &proof.premises, &prelude, elaborator_config)
.elaborate_with_default_pipeline(&node);
let elaborated = ast::Proof {
premises: proof.premises,
commands: elaborated.into_commands(),
Expand Down
22 changes: 6 additions & 16 deletions carcara/tests/test_example_files.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -48,14 +48,9 @@ fn run_test(problem_path: &Path, proof_path: &Path) -> CarcaraResult<()> {
resolution_granularity: elaborator::ResolutionGranularity::Reordering,
};
let node = ast::ProofNode::from_commands(proof.commands.clone());
let elaborated_node = elaborator::elaborate(
&mut pool,
&proof.premises,
&prelude,
&node,
config.clone(),
elaborator::default_pipeline(),
);
let elaborated_node =
elaborator::Elaborator::new(&mut pool, &proof.premises, &prelude, config.clone())
.elaborate_with_default_pipeline(&node);
let elaborated = ast::Proof {
premises: proof.premises.clone(),
commands: elaborated_node.into_commands(),
Expand All @@ -66,14 +61,9 @@ fn run_test(problem_path: &Path, proof_path: &Path) -> CarcaraResult<()> {

// Finally, we elaborate the already elaborated proof, to make sure the elaboration step is
// idempotent
let elaborated_twice = elaborator::elaborate(
&mut pool,
&proof.premises,
&prelude,
&elaborated_node,
config,
elaborator::default_pipeline(),
);
let elaborated_twice =
elaborator::Elaborator::new(&mut pool, &proof.premises, &prelude, config)
.elaborate_with_default_pipeline(&elaborated_node);
assert!(
elaborated.commands == elaborated_twice.into_commands(),
"elaboration was not idempotent!"
Expand Down
10 changes: 2 additions & 8 deletions cli/src/benchmarking.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -55,14 +55,8 @@ fn run_job<T: CollectResults + Default + Send>(
let elaboration = if let Some(config) = elaborator_config {
let elaboration = Instant::now();
let node = ast::ProofNode::from_commands(proof.commands);
let elaborated = elaborator::elaborate(
&mut pool,
&proof.premises,
&prelude,
&node,
config,
elaborator::default_pipeline(),
);
let elaborated = elaborator::Elaborator::new(&mut pool, &proof.premises, &prelude, config)
.elaborate_with_default_pipeline(&node);
elaborated.into_commands();
elaboration.elapsed()
} else {
Expand Down

0 comments on commit f380239

Please sign in to comment.