Skip to content

Commit b1c638c

Browse files
coord-ecoord-e
authored
Merge pull request #1 from coord-e/more-annot
Support logical connectives in annotations
2 parents 914bedd + 30ed351 commit b1c638c

File tree

20 files changed

+1133
-552
lines changed

20 files changed

+1133
-552
lines changed

‎.github/workflows/ci.yml‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -10,13 +10,15 @@ jobs:
1010
contents: read
1111
steps:
1212
- uses: actions/checkout@v4
13+
- run: rustup component add rustfmt
1314
- run: cargo fmt --all -- --check
1415
clippy:
1516
runs-on: ubuntu-latest
1617
permissions:
1718
contents: read
1819
steps:
1920
- uses: actions/checkout@v4
21+
- run: rustup component add clippy
2022
- run: cargo clippy -- -D warnings
2123
test:
2224
runs-on: ubuntu-latest

‎src/analyze.rs‎

Lines changed: 0 additions & 23 deletions
Original file line numberDiff line numberDiff line change
@@ -137,29 +137,6 @@ impl<'tcx> Analyzer<'tcx> {
137137
.borrow_mut()
138138
.new_pred_var(sig, chc::DebugInfo::from_current_span())
139139
}
140-
141-
fn implied_atom<FV, F>(&mut self, atoms: Vec<chc::Atom<FV>>, mut fv_sort: F) -> chc::Atom<FV>
142-
where
143-
F: FnMut(FV) -> chc::Sort,
144-
FV: chc::Var + std::fmt::Debug + Clone,
145-
{
146-
let fvs: Vec<_> = atoms.iter().flat_map(|a| a.fv()).cloned().collect();
147-
let mut builder = chc::ClauseBuilder::default();
148-
let mut pred_sig = chc::PredSig::new();
149-
for fv in &fvs {
150-
let sort = fv_sort(*fv);
151-
builder.add_mapped_var(*fv, sort.clone());
152-
pred_sig.push(sort);
153-
}
154-
for atom in atoms {
155-
builder.add_body_mapped(atom);
156-
}
157-
let pv = self.generate_pred_var(pred_sig);
158-
let head = chc::Atom::new(pv.into(), fvs.into_iter().map(chc::Term::var).collect());
159-
let clause = builder.head_mapped(head.clone());
160-
self.add_clause(clause);
161-
head
162-
}
163140
}
164141

165142
impl<'tcx> Analyzer<'tcx> {

‎src/analyze/annot.rs‎

Lines changed: 11 additions & 25 deletions
Original file line numberDiff line numberDiff line change
@@ -1,10 +1,10 @@
11
use rustc_ast::ast::Attribute;
22
use rustc_ast::tokenstream::TokenStream;
33
use rustc_index::IndexVec;
4-
use rustc_middle::ty as mir_ty;
54
use rustc_span::symbol::{Ident, Symbol};
65

76
use crate::annot;
7+
use crate::chc;
88
use crate::rty;
99

1010
pub fn requires_path() -> [Symbol; 2] {
@@ -31,64 +31,50 @@ pub fn callable_path() -> [Symbol; 2] {
3131
[Symbol::intern("thrust"), Symbol::intern("callable")]
3232
}
3333

34-
fn ty_to_term_kind(ty: &mir_ty::Ty<'_>) -> annot::TermKind {
35-
match ty.kind() {
36-
mir_ty::TyKind::Ref(_, ty, mir_ty::Mutability::Mut) => {
37-
annot::TermKind::mut_(ty_to_term_kind(ty))
38-
}
39-
mir_ty::TyKind::Ref(_, ty, mir_ty::Mutability::Not) => {
40-
annot::TermKind::box_(ty_to_term_kind(ty))
41-
}
42-
mir_ty::TyKind::Adt(def, _) if def.is_box() => annot::TermKind::box_(ty_to_term_kind(ty)),
43-
_ => annot::TermKind::other(),
44-
}
45-
}
46-
4734
#[derive(Debug, Clone, Default)]
4835
pub struct ParamResolver {
49-
params: IndexVec<rty::FunctionParamIdx, (Symbol, annot::TermKind)>,
36+
params: IndexVec<rty::FunctionParamIdx, (Symbol, chc::Sort)>,
5037
}
5138

5239
impl annot::Resolver for ParamResolver {
5340
type Output = rty::FunctionParamIdx;
54-
fn resolve(&self, ident: Ident) -> Option<(Self::Output, annot::TermKind)> {
41+
fn resolve(&self, ident: Ident) -> Option<(Self::Output, chc::Sort)> {
5542
self.params
5643
.iter_enumerated()
5744
.find(|(_, (name, _))| name == &ident.name)
58-
.map(|(idx, (_, kind))| (idx, kind.clone()))
45+
.map(|(idx, (_, sort))| (idx, sort.clone()))
5946
}
6047
}
6148

6249
impl ParamResolver {
63-
pub fn push_param(&mut self, name: Symbol, ty: &mir_ty::Ty<'_>) {
64-
self.params.push((name, ty_to_term_kind(ty)));
50+
pub fn push_param(&mut self, name: Symbol, sort: chc::Sort) {
51+
self.params.push((name, sort));
6552
}
6653
}
6754

6855
#[derive(Debug, Clone)]
6956
pub struct ResultResolver {
7057
result_symbol: Symbol,
71-
result_kind: annot::TermKind,
58+
result_sort: chc::Sort,
7259
}
7360

7461
impl annot::Resolver for ResultResolver {
7562
type Output = rty::RefinedTypeVar<rty::FunctionParamIdx>;
76-
fn resolve(&self, ident: Ident) -> Option<(Self::Output, annot::TermKind)> {
63+
fn resolve(&self, ident: Ident) -> Option<(Self::Output, chc::Sort)> {
7764
if ident.name == self.result_symbol {
78-
Some((rty::RefinedTypeVar::Value, self.result_kind.clone()))
65+
Some((rty::RefinedTypeVar::Value, self.result_sort.clone()))
7966
} else {
8067
None
8168
}
8269
}
8370
}
8471

8572
impl ResultResolver {
86-
pub fn new(result_ty: &mir_ty::Ty<'_>) -> Self {
73+
pub fn new(result_sort: chc::Sort) -> Self {
8774
let result_symbol = Symbol::intern("result");
88-
let result_kind = ty_to_term_kind(result_ty);
8975
Self {
9076
result_symbol,
91-
result_kind,
77+
result_sort,
9278
}
9379
}
9480
}

‎src/analyze/basic_block.rs‎

Lines changed: 54 additions & 51 deletions
Original file line numberDiff line numberDiff line change
@@ -101,23 +101,23 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> {
101101
}
102102
for ((param_idx, got_ty), expected_ty) in got.params.iter_enumerated().zip(&expected_args) {
103103
// TODO we can use relate_sub_refined_type here when we implemenented builder-aware relate_*
104-
let clause = builder
104+
let cs = builder
105105
.clone()
106106
.with_value_var(&got_ty.ty)
107107
.add_body(expected_ty.refinement.clone())
108108
.head(got_ty.refinement.clone());
109-
clauses.push(clause);
109+
clauses.extend(cs);
110110
builder
111111
.with_mapped_value_var(param_idx)
112112
.add_body(expected_ty.refinement.clone());
113113
clauses.extend(builder.relate_sub_type(&expected_ty.ty, &got_ty.ty));
114114
}
115115

116-
let clause = builder
116+
let cs = builder
117117
.with_value_var(&got.ret.ty)
118118
.add_body(got.ret.refinement)
119119
.head(expected_ret.refinement);
120-
clauses.push(clause);
120+
clauses.extend(cs);
121121
clauses.extend(builder.relate_sub_type(&got.ret.ty, &expected_ret.ty));
122122
clauses
123123
}
@@ -450,10 +450,8 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> {
450450
let ret2 = chc::Term::var(param2_var)
451451
.mut_current()
452452
.equal_to(chc::Term::var(param1_var).mut_final());
453-
let ret_refinement = self
454-
.ctx
455-
.implied_atom(vec![ret1, ret2], |_| param1.ty.to_sort());
456-
let ret = rty::RefinedType::new(rty::Type::unit(), ret_refinement.into());
453+
let ret_formula = chc::Formula::Atom(ret1).and(chc::Formula::Atom(ret2));
454+
let ret = rty::RefinedType::new(rty::Type::unit(), ret_formula.into());
457455
rty::FunctionType::new([param1, param2].into_iter().collect(), ret).into()
458456
}
459457
Some((def_id, args)) => {
@@ -758,30 +756,37 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> {
758756
}
759757
}
760758

759+
/// Turns [`rty::RefinedType<Var>`] into [`rty::RefinedType<T>`].
760+
///
761+
/// We sometimes need to replace [`rty::RefinedTypeVar<Var>`] with [`rty::RefinedTypeVar<T>`].
762+
/// In [`analyze::basic_block`] module, `T` is [`rty::FunctionParamIdx`]. The type we get as
763+
/// a function result is obtained as [`rty::RefinedTypeVar<Var>`], but we need to express it using
764+
/// only function parameters for the subtyping. [`UnbindAtoms`] holds the relation between
765+
/// the function parameters and their representaion under the environment and
766+
/// let the type in environment be expressed only under the function parameters using existentials.
761767
#[derive(Debug, Clone)]
762768
pub struct UnbindAtoms<T> {
763769
existentials: IndexVec<rty::ExistentialVarIdx, chc::Sort>,
764-
atoms: Vec<chc::Atom<rty::RefinedTypeVar<Var>>>,
770+
formula: rty::FormulaWithAtoms<rty::RefinedTypeVar<Var>>,
765771
target_equations: Vec<(rty::RefinedTypeVar<T>, chc::Term<rty::RefinedTypeVar<Var>>)>,
766772
}
767773

768774
impl<T> Default for UnbindAtoms<T> {
769775
fn default() -> Self {
770776
UnbindAtoms {
771777
existentials: Default::default(),
772-
atoms: Default::default(),
778+
formula: Default::default(),
773779
target_equations: Default::default(),
774780
}
775781
}
776782
}
777783

778784
impl<T> UnbindAtoms<T> {
779785
pub fn push(&mut self, target: rty::RefinedTypeVar<T>, var_ty: PlaceType) {
780-
self.atoms.extend(
786+
self.formula.push_conj(
781787
var_ty
782-
.conds
783-
.into_iter()
784-
.map(|a| a.map_var(|v| v.shift_existential(self.existentials.len()).into())),
788+
.formula
789+
.map_var(|v| v.shift_existential(self.existentials.len()).into()),
785790
);
786791
self.target_equations.push((
787792
target,
@@ -799,14 +804,11 @@ impl<T> UnbindAtoms<T> {
799804
} = ty;
800805
let rty::Refinement {
801806
existentials,
802-
atoms,
807+
formula,
803808
} = refinement;
804809

805-
self.atoms.extend(
806-
atoms
807-
.into_iter()
808-
.map(|a| a.map_var(|v| v.shift_existential(self.existentials.len()))),
809-
);
810+
self.formula
811+
.push_conj(formula.map_var(|v| v.shift_existential(self.existentials.len())));
810812
self.existentials.extend(existentials);
811813

812814
let mut substs = HashMap::new();
@@ -815,25 +817,29 @@ impl<T> UnbindAtoms<T> {
815817
substs.insert(v, ev);
816818
}
817819

818-
let atoms = self
819-
.atoms
820-
.into_iter()
821-
.map(|a| {
822-
a.map_var(|v| match v {
823-
rty::RefinedTypeVar::Value => rty::RefinedTypeVar::Value,
824-
rty::RefinedTypeVar::Free(v) => rty::RefinedTypeVar::Existential(substs[&v]),
825-
rty::RefinedTypeVar::Existential(ev) => rty::RefinedTypeVar::Existential(ev),
820+
let mut formula = self.formula.map_var(|v| match v {
821+
rty::RefinedTypeVar::Value => rty::RefinedTypeVar::Value,
822+
rty::RefinedTypeVar::Free(v) => rty::RefinedTypeVar::Existential(substs[&v]),
823+
rty::RefinedTypeVar::Existential(ev) => rty::RefinedTypeVar::Existential(ev),
824+
});
825+
formula.push_conj(
826+
self.target_equations
827+
.into_iter()
828+
.map(|(t, term)| {
829+
chc::Term::var(t).equal_to(term.map_var(|v| match v {
830+
rty::RefinedTypeVar::Value => rty::RefinedTypeVar::Value,
831+
rty::RefinedTypeVar::Free(v) => {
832+
rty::RefinedTypeVar::Existential(substs[&v])
833+
}
834+
rty::RefinedTypeVar::Existential(ev) => {
835+
rty::RefinedTypeVar::Existential(ev)
836+
}
837+
}))
826838
})
827-
})
828-
.chain(self.target_equations.into_iter().map(|(t, term)| {
829-
chc::Term::var(t).equal_to(term.map_var(|v| match v {
830-
rty::RefinedTypeVar::Value => rty::RefinedTypeVar::Value,
831-
rty::RefinedTypeVar::Free(v) => rty::RefinedTypeVar::Existential(substs[&v]),
832-
rty::RefinedTypeVar::Existential(ev) => rty::RefinedTypeVar::Existential(ev),
833-
}))
834-
}))
835-
.collect();
836-
let refinement = rty::Refinement::new(self.existentials, atoms);
839+
.collect::<Vec<_>>(),
840+
);
841+
842+
let refinement = rty::Refinement::with_formula(self.existentials, formula);
837843
// TODO: polymorphic datatypes: template needed?
838844
rty::RefinedType::new(src_ty.assert_closed().vacuous(), refinement)
839845
}
@@ -872,11 +878,10 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> {
872878
}
873879

874880
let local_ty = self.env.local_type(local);
875-
assumption.conds.extend(
881+
assumption.formula.push_conj(
876882
local_ty
877-
.conds
878-
.into_iter()
879-
.map(|a| a.map_var(|v| v.shift_existential(assumption.existentials.len()))),
883+
.formula
884+
.map_var(|v| v.shift_existential(assumption.existentials.len())),
880885
);
881886
let term = local_ty
882887
.term
@@ -889,16 +894,14 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> {
889894
for (idx, param) in expected_params.iter_enumerated() {
890895
let rty::Refinement {
891896
existentials,
892-
atoms,
897+
formula,
893898
} = param.refinement.clone();
894-
assumption.conds.extend(atoms.into_iter().map(|a| {
895-
a.subst_var(|v| match v {
896-
rty::RefinedTypeVar::Value => param_terms[&idx].clone(),
897-
rty::RefinedTypeVar::Free(v) => param_terms[&v].clone(),
898-
rty::RefinedTypeVar::Existential(ev) => chc::Term::var(
899-
PlaceTypeVar::Existential(ev + assumption.existentials.len()),
900-
),
901-
})
899+
assumption.formula.push_conj(formula.subst_var(|v| match v {
900+
rty::RefinedTypeVar::Value => param_terms[&idx].clone(),
901+
rty::RefinedTypeVar::Free(v) => param_terms[&v].clone(),
902+
rty::RefinedTypeVar::Existential(ev) => chc::Term::var(PlaceTypeVar::Existential(
903+
ev + assumption.existentials.len(),
904+
)),
902905
}));
903906
assumption.existentials.extend(existentials);
904907
}

0 commit comments

Comments
 (0)