Skip to content

Commit

Permalink
Merge pull request #602 from detrumi/simplify-lowering
Browse files Browse the repository at this point in the history
Simplify lowering
  • Loading branch information
detrumi authored Sep 7, 2020
2 parents cf7bc67 + db471f1 commit 99ea62d
Show file tree
Hide file tree
Showing 8 changed files with 538 additions and 872 deletions.
4 changes: 2 additions & 2 deletions chalk-integration/src/db.rs
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
use crate::{
error::ChalkError,
interner::ChalkIr,
lowering::LowerGoal,
lowering::lower_goal,
program::Program,
query::{Lowering, LoweringDatabase},
tls, SolverChoice,
Expand Down Expand Up @@ -43,7 +43,7 @@ impl ChalkDatabase {

pub fn parse_and_lower_goal(&self, text: &str) -> Result<Goal<ChalkIr>, ChalkError> {
let program = self.checked_program()?;
Ok(chalk_parse::parse_goal(text)?.lower(&*program)?)
Ok(lower_goal(&*chalk_parse::parse_goal(text)?, &*program)?)
}

pub fn solve(
Expand Down
1,364 changes: 513 additions & 851 deletions chalk-integration/src/lowering.rs

Large diffs are not rendered by default.

2 changes: 1 addition & 1 deletion chalk-integration/src/query.rs
Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,7 @@

use crate::error::ChalkError;
use crate::interner::ChalkIr;
use crate::lowering::LowerProgram;
use crate::lowering::Lower;
use crate::program::Program;
use crate::program_environment::ProgramEnvironment;
use crate::tls;
Expand Down
2 changes: 1 addition & 1 deletion chalk-parse/src/ast.rs
Original file line number Diff line number Diff line change
Expand Up @@ -151,7 +151,7 @@ pub struct AssocTyDefn {
pub struct OpaqueTyDefn {
pub ty: Ty,
pub variable_kinds: Vec<VariableKind>,
pub identifier: Identifier,
pub name: Identifier,
pub bounds: Vec<QuantifiedInlineBound>,
pub where_clauses: Vec<QuantifiedWhereClause>,
}
Expand Down
4 changes: 2 additions & 2 deletions chalk-parse/src/parser.lalrpop
Original file line number Diff line number Diff line change
Expand Up @@ -231,12 +231,12 @@ AssocTyDefn: AssocTyDefn = {
};

OpaqueTyDefn: OpaqueTyDefn = {
"opaque" "type" <identifier:Id> <p:Angle<VariableKind>> ":" <b:Plus<QuantifiedInlineBound>>
"opaque" "type" <name:Id> <p:Angle<VariableKind>> ":" <b:Plus<QuantifiedInlineBound>>
<w:QuantifiedWhereClauses> "=" <ty:Ty> ";" => {
OpaqueTyDefn {
ty,
variable_kinds: p,
identifier,
name,
bounds: b,
where_clauses: w,
}
Expand Down
2 changes: 1 addition & 1 deletion src/main.rs
Original file line number Diff line number Diff line change
Expand Up @@ -66,7 +66,7 @@ impl LoadedProgram {
multiple_answers: bool,
) -> Result<()> {
let program = self.db.checked_program()?;
let goal = chalk_parse::parse_goal(text)?.lower(&*program)?;
let goal = lower_goal(&*chalk_parse::parse_goal(text)?, &*program)?;
let peeled_goal = goal.into_peeled_goal(self.db.interner());
if multiple_answers {
if self.db.solve_multiple(&peeled_goal, &mut |v, has_next| {
Expand Down
21 changes: 12 additions & 9 deletions tests/logging_db/util.rs
Original file line number Diff line number Diff line change
Expand Up @@ -5,7 +5,8 @@
//! to `test/`. We can't compile without access to `test/`, so we can't be under
//! of `test_util.rs`.
use chalk_integration::{
db::ChalkDatabase, lowering::LowerGoal, program::Program, query::LoweringDatabase, SolverChoice,
db::ChalkDatabase, lowering::lower_goal, program::Program, query::LoweringDatabase,
SolverChoice,
};
use chalk_solve::ext::*;
use chalk_solve::logging_db::LoggingRustIrDatabase;
Expand Down Expand Up @@ -47,10 +48,11 @@ pub fn logging_db_output_sufficient(
println!("goal {}", goal_text);
assert!(goal_text.starts_with("{"));
assert!(goal_text.ends_with("}"));
let goal = chalk_parse::parse_goal(&goal_text[1..goal_text.len() - 1])
.unwrap()
.lower(&*program)
.unwrap();
let goal = lower_goal(
&*chalk_parse::parse_goal(&goal_text[1..goal_text.len() - 1]).unwrap(),
&*program,
)
.unwrap();

println!("using solver: {:?}", solver_choice);
let peeled_goal = goal.into_peeled_goal(db.interner());
Expand Down Expand Up @@ -88,10 +90,11 @@ pub fn logging_db_output_sufficient(
println!("goal {}", goal_text);
assert!(goal_text.starts_with("{"));
assert!(goal_text.ends_with("}"));
let goal = chalk_parse::parse_goal(&goal_text[1..goal_text.len() - 1])
.unwrap()
.lower(&*new_program)
.unwrap();
let goal = lower_goal(
&*chalk_parse::parse_goal(&goal_text[1..goal_text.len() - 1]).unwrap(),
&*new_program,
)
.unwrap();

println!("using solver: {:?}", solver_choice);
let peeled_goal = goal.into_peeled_goal(db.interner());
Expand Down
11 changes: 6 additions & 5 deletions tests/test/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,7 @@
use crate::test_util::assert_same;
use chalk_integration::db::ChalkDatabase;
use chalk_integration::interner::ChalkIr;
use chalk_integration::lowering::LowerGoal;
use chalk_integration::lowering::lower_goal;
use chalk_integration::query::LoweringDatabase;
use chalk_integration::SolverChoice;
use chalk_ir::Constraints;
Expand Down Expand Up @@ -254,10 +254,11 @@ fn solve_goal(program_text: &str, goals: Vec<(&str, SolverChoice, TestGoal)>, co
println!("goal {}", goal_text);
assert!(goal_text.starts_with("{"));
assert!(goal_text.ends_with("}"));
let goal = chalk_parse::parse_goal(&goal_text[1..goal_text.len() - 1])
.unwrap()
.lower(&*program)
.unwrap();
let goal = lower_goal(
&*chalk_parse::parse_goal(&goal_text[1..goal_text.len() - 1]).unwrap(),
&*program,
)
.unwrap();

println!("using solver: {:?}", solver_choice);
let peeled_goal = goal.into_peeled_goal(db.interner());
Expand Down

0 comments on commit 99ea62d

Please sign in to comment.