Skip to content

Commit 583f66a

Browse files
coord-ecoord-e
authored
Merge pull request #3 from coord-e/unify-formula
Define rty::Formula and replace UnboundAssumption and Refinement with it
2 parents b1c638c + 43ba71b commit 583f66a

12 files changed

Lines changed: 359 additions & 451 deletions

File tree

‎src/analyze/basic_block.rs‎

Lines changed: 20 additions & 28 deletions
Original file line numberDiff line numberDiff line change
@@ -13,10 +13,12 @@ use crate::analyze;
1313
use crate::chc;
1414
use crate::pretty::PrettyDisplayExt as _;
1515
use crate::refine::{
16-
self, BasicBlockType, Env, PlaceType, PlaceTypeVar, TempVarIdx, TemplateTypeGenerator,
17-
UnboundAssumption, UnrefinedTypeGenerator, Var,
16+
self, Assumption, BasicBlockType, Env, PlaceType, PlaceTypeVar, TempVarIdx,
17+
TemplateTypeGenerator, UnrefinedTypeGenerator, Var,
18+
};
19+
use crate::rty::{
20+
self, ClauseBuilderExt as _, ClauseScope as _, ShiftExistential as _, Subtyping as _,
1821
};
19-
use crate::rty::{self, ClauseBuilderExt as _, ClauseScope as _, Subtyping as _};
2022

2123
mod drop_point;
2224
mod visitor;
@@ -339,11 +341,7 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> {
339341
self.ctx.extend_clauses(clauses);
340342
}
341343

342-
fn with_assumptions<F, T>(
343-
&mut self,
344-
assumptions: Vec<impl Into<UnboundAssumption>>,
345-
callback: F,
346-
) -> T
344+
fn with_assumptions<F, T>(&mut self, assumptions: Vec<impl Into<Assumption>>, callback: F) -> T
347345
where
348346
F: FnOnce(&mut Self) -> T,
349347
{
@@ -354,7 +352,7 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> {
354352
result
355353
}
356354

357-
fn with_assumption<F, T>(&mut self, assumption: impl Into<UnboundAssumption>, callback: F) -> T
355+
fn with_assumption<F, T>(&mut self, assumption: impl Into<Assumption>, callback: F) -> T
358356
where
359357
F: FnOnce(&mut Self) -> T,
360358
{
@@ -767,23 +765,23 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> {
767765
#[derive(Debug, Clone)]
768766
pub struct UnbindAtoms<T> {
769767
existentials: IndexVec<rty::ExistentialVarIdx, chc::Sort>,
770-
formula: rty::FormulaWithAtoms<rty::RefinedTypeVar<Var>>,
768+
body: chc::Body<rty::RefinedTypeVar<Var>>,
771769
target_equations: Vec<(rty::RefinedTypeVar<T>, chc::Term<rty::RefinedTypeVar<Var>>)>,
772770
}
773771

774772
impl<T> Default for UnbindAtoms<T> {
775773
fn default() -> Self {
776774
UnbindAtoms {
777775
existentials: Default::default(),
778-
formula: Default::default(),
776+
body: Default::default(),
779777
target_equations: Default::default(),
780778
}
781779
}
782780
}
783781

784782
impl<T> UnbindAtoms<T> {
785783
pub fn push(&mut self, target: rty::RefinedTypeVar<T>, var_ty: PlaceType) {
786-
self.formula.push_conj(
784+
self.body.push_conj(
787785
var_ty
788786
.formula
789787
.map_var(|v| v.shift_existential(self.existentials.len()).into()),
@@ -802,13 +800,10 @@ impl<T> UnbindAtoms<T> {
802800
ty: src_ty,
803801
refinement,
804802
} = ty;
805-
let rty::Refinement {
806-
existentials,
807-
formula,
808-
} = refinement;
803+
let rty::Refinement { existentials, body } = refinement;
809804

810-
self.formula
811-
.push_conj(formula.map_var(|v| v.shift_existential(self.existentials.len())));
805+
self.body
806+
.push_conj(body.map_var(|v| v.shift_existential(self.existentials.len())));
812807
self.existentials.extend(existentials);
813808

814809
let mut substs = HashMap::new();
@@ -817,12 +812,12 @@ impl<T> UnbindAtoms<T> {
817812
substs.insert(v, ev);
818813
}
819814

820-
let mut formula = self.formula.map_var(|v| match v {
815+
let mut body = self.body.map_var(|v| match v {
821816
rty::RefinedTypeVar::Value => rty::RefinedTypeVar::Value,
822817
rty::RefinedTypeVar::Free(v) => rty::RefinedTypeVar::Existential(substs[&v]),
823818
rty::RefinedTypeVar::Existential(ev) => rty::RefinedTypeVar::Existential(ev),
824819
});
825-
formula.push_conj(
820+
body.push_conj(
826821
self.target_equations
827822
.into_iter()
828823
.map(|(t, term)| {
@@ -839,7 +834,7 @@ impl<T> UnbindAtoms<T> {
839834
.collect::<Vec<_>>(),
840835
);
841836

842-
let refinement = rty::Refinement::with_formula(self.existentials, formula);
837+
let refinement = rty::Refinement::new(self.existentials, body);
843838
// TODO: polymorphic datatypes: template needed?
844839
rty::RefinedType::new(src_ty.assert_closed().vacuous(), refinement)
845840
}
@@ -852,7 +847,7 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> {
852847
expected_params: &IndexVec<rty::FunctionParamIdx, rty::RefinedType<rty::FunctionParamIdx>>,
853848
) {
854849
let mut param_terms = HashMap::<rty::FunctionParamIdx, chc::Term<PlaceTypeVar>>::new();
855-
let mut assumption = UnboundAssumption::default();
850+
let mut assumption = Assumption::default();
856851

857852
let bb_ty = self.basic_block_ty(self.basic_block).clone();
858853
let params = &bb_ty.as_ref().params;
@@ -878,7 +873,7 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> {
878873
}
879874

880875
let local_ty = self.env.local_type(local);
881-
assumption.formula.push_conj(
876+
assumption.body.push_conj(
882877
local_ty
883878
.formula
884879
.map_var(|v| v.shift_existential(assumption.existentials.len())),
@@ -892,11 +887,8 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> {
892887
}
893888

894889
for (idx, param) in expected_params.iter_enumerated() {
895-
let rty::Refinement {
896-
existentials,
897-
formula,
898-
} = param.refinement.clone();
899-
assumption.formula.push_conj(formula.subst_var(|v| match v {
890+
let rty::Refinement { existentials, body } = param.refinement.clone();
891+
assumption.body.push_conj(body.subst_var(|v| match v {
900892
rty::RefinedTypeVar::Value => param_terms[&idx].clone(),
901893
rty::RefinedTypeVar::Free(v) => param_terms[&v].clone(),
902894
rty::RefinedTypeVar::Existential(ev) => chc::Term::var(PlaceTypeVar::Existential(

‎src/chc.rs‎

Lines changed: 152 additions & 24 deletions
Original file line numberDiff line numberDiff line change
@@ -1193,16 +1193,16 @@ impl<V> Formula<V> {
11931193
}
11941194
}
11951195

1196-
pub fn atoms(&self) -> impl Iterator<Item = &Atom<V>> {
1197-
self.atoms_impl()
1196+
pub fn iter_atoms(&self) -> impl Iterator<Item = &Atom<V>> {
1197+
self.iter_atoms_impl()
11981198
}
11991199

1200-
fn atoms_impl(&self) -> Box<dyn Iterator<Item = &Atom<V>> + '_> {
1200+
fn iter_atoms_impl(&self) -> Box<dyn Iterator<Item = &Atom<V>> + '_> {
12011201
match self {
12021202
Formula::Atom(atom) => Box::new(std::iter::once(atom)),
1203-
Formula::Not(fo) => Box::new(fo.atoms()),
1204-
Formula::And(fs) => Box::new(fs.iter().flat_map(Formula::atoms)),
1205-
Formula::Or(fs) => Box::new(fs.iter().flat_map(Formula::atoms)),
1203+
Formula::Not(fo) => Box::new(fo.iter_atoms()),
1204+
Formula::And(fs) => Box::new(fs.iter().flat_map(Formula::iter_atoms)),
1205+
Formula::Or(fs) => Box::new(fs.iter().flat_map(Formula::iter_atoms)),
12061206
}
12071207
}
12081208

@@ -1248,13 +1248,154 @@ impl<V> Formula<V> {
12481248
}
12491249
}
12501250

1251+
#[derive(Debug, Clone)]
1252+
pub struct Body<V = TermVarIdx> {
1253+
pub atoms: Vec<Atom<V>>,
1254+
// `formula` doesn't contain PredVar
1255+
pub formula: Formula<V>,
1256+
}
1257+
1258+
impl<V> Default for Body<V> {
1259+
fn default() -> Self {
1260+
Body {
1261+
atoms: Default::default(),
1262+
formula: Default::default(),
1263+
}
1264+
}
1265+
}
1266+
1267+
impl<V> From<Atom<V>> for Body<V> {
1268+
fn from(atom: Atom<V>) -> Self {
1269+
Body {
1270+
atoms: vec![atom],
1271+
formula: Formula::top(),
1272+
}
1273+
}
1274+
}
1275+
1276+
impl<V> From<Vec<Atom<V>>> for Body<V> {
1277+
fn from(atoms: Vec<Atom<V>>) -> Self {
1278+
Body {
1279+
atoms,
1280+
formula: Formula::top(),
1281+
}
1282+
}
1283+
}
1284+
1285+
impl<V> From<Formula<V>> for Body<V> {
1286+
fn from(formula: Formula<V>) -> Self {
1287+
Body {
1288+
atoms: vec![],
1289+
formula,
1290+
}
1291+
}
1292+
}
1293+
1294+
impl<V> Body<V> {
1295+
pub fn new(atoms: Vec<Atom<V>>, formula: Formula<V>) -> Self {
1296+
Body { atoms, formula }
1297+
}
1298+
1299+
pub fn top() -> Self {
1300+
Body {
1301+
atoms: vec![],
1302+
formula: Formula::top(),
1303+
}
1304+
}
1305+
1306+
pub fn bottom() -> Self {
1307+
Body {
1308+
atoms: vec![],
1309+
formula: Formula::bottom(),
1310+
}
1311+
}
1312+
1313+
pub fn is_top(&self) -> bool {
1314+
self.formula.is_top() && self.atoms.iter().all(|a| a.is_top())
1315+
}
1316+
1317+
pub fn is_bottom(&self) -> bool {
1318+
self.formula.is_bottom() || self.atoms.iter().any(|a| a.is_bottom())
1319+
}
1320+
1321+
pub fn push_conj(&mut self, other: impl Into<Body<V>>) {
1322+
let Body { atoms, formula } = other.into();
1323+
self.atoms.extend(atoms);
1324+
self.formula.push_conj(formula);
1325+
}
1326+
1327+
pub fn map_var<F, W>(self, mut f: F) -> Body<W>
1328+
where
1329+
F: FnMut(V) -> W,
1330+
{
1331+
Body {
1332+
atoms: self.atoms.into_iter().map(|a| a.map_var(&mut f)).collect(),
1333+
formula: self.formula.map_var(f),
1334+
}
1335+
}
1336+
1337+
pub fn subst_var<F, W>(self, mut f: F) -> Body<W>
1338+
where
1339+
F: FnMut(V) -> Term<W>,
1340+
{
1341+
Body {
1342+
atoms: self
1343+
.atoms
1344+
.into_iter()
1345+
.map(|a| a.subst_var(&mut f))
1346+
.collect(),
1347+
formula: self.formula.subst_var(f),
1348+
}
1349+
}
1350+
1351+
pub fn simplify(&mut self) {
1352+
self.formula.simplify();
1353+
self.atoms.retain(|a| !a.is_top());
1354+
if self.is_bottom() {
1355+
self.atoms = vec![Atom::bottom()];
1356+
self.formula = Formula::top();
1357+
}
1358+
}
1359+
1360+
pub fn iter_atoms(&self) -> impl Iterator<Item = &Atom<V>> {
1361+
self.formula.iter_atoms().chain(&self.atoms)
1362+
}
1363+
}
1364+
1365+
impl<'a, 'b, D, V> Pretty<'a, D, termcolor::ColorSpec> for &'b Body<V>
1366+
where
1367+
V: Var,
1368+
D: pretty::DocAllocator<'a, termcolor::ColorSpec>,
1369+
D::Doc: Clone,
1370+
{
1371+
fn pretty(self, allocator: &'a D) -> pretty::DocBuilder<'a, D, termcolor::ColorSpec> {
1372+
let atoms = allocator.intersperse(
1373+
&self.atoms,
1374+
allocator
1375+
.text("∧")
1376+
.enclose(allocator.line(), allocator.space()),
1377+
);
1378+
let formula = self.formula.pretty(allocator);
1379+
if self.atoms.is_empty() {
1380+
formula
1381+
} else if self.formula.is_top() {
1382+
atoms.group()
1383+
} else {
1384+
atoms
1385+
.append(allocator.line())
1386+
.append(allocator.text("∧"))
1387+
.append(allocator.line())
1388+
.append(formula)
1389+
.group()
1390+
}
1391+
}
1392+
}
1393+
12511394
#[derive(Debug, Clone)]
12521395
pub struct Clause {
12531396
pub vars: IndexVec<TermVarIdx, Sort>,
12541397
pub head: Atom<TermVarIdx>,
1255-
pub body_atoms: Vec<Atom<TermVarIdx>>,
1256-
// body_formula doesn't contain PredVar
1257-
pub body_formula: Formula<TermVarIdx>,
1398+
pub body: Body<TermVarIdx>,
12581399
pub debug_info: DebugInfo,
12591400
}
12601401

@@ -1272,7 +1413,7 @@ where
12721413
allocator.text(",").append(allocator.line()),
12731414
)
12741415
.group();
1275-
let body = self.body().pretty(allocator);
1416+
let body = self.body.pretty(allocator);
12761417
let imp = self
12771418
.head
12781419
.pretty(allocator)
@@ -1291,21 +1432,8 @@ where
12911432
}
12921433

12931434
impl Clause {
1294-
pub fn body(&self) -> Formula {
1295-
Formula::And(
1296-
self.body_atoms
1297-
.clone()
1298-
.into_iter()
1299-
.map(Formula::from)
1300-
.collect(),
1301-
)
1302-
.and(self.body_formula.clone())
1303-
}
1304-
13051435
pub fn is_nop(&self) -> bool {
1306-
self.head.is_top()
1307-
|| self.body_atoms.iter().any(Atom::is_bottom)
1308-
|| self.body_formula.is_bottom()
1436+
self.head.is_top() || self.body.is_bottom()
13091437
}
13101438

13111439
fn term_sort(&self, term: &Term<TermVarIdx>) -> Sort {

0 commit comments

Comments
 (0)