Support logical connectives in annotations

.github/workflows/ci.yml

@@ -10,13 +10,15 @@ jobs:
       contents: read
     steps:
       - uses: actions/checkout@v4
+      - run: rustup component add rustfmt
       - run: cargo fmt --all -- --check
   clippy:
     runs-on: ubuntu-latest
     permissions:
       contents: read
     steps:
       - uses: actions/checkout@v4
+      - run: rustup component add clippy
       - run: cargo clippy -- -D warnings
   test:
     runs-on: ubuntu-latest

src/analyze.rs

@@ -137,29 +137,6 @@ impl<'tcx> Analyzer<'tcx> {
             .borrow_mut()
             .new_pred_var(sig, chc::DebugInfo::from_current_span())
     }
-
-    fn implied_atom<FV, F>(&mut self, atoms: Vec<chc::Atom<FV>>, mut fv_sort: F) -> chc::Atom<FV>
-    where
-        F: FnMut(FV) -> chc::Sort,
-        FV: chc::Var + std::fmt::Debug + Clone,
-    {
-        let fvs: Vec<_> = atoms.iter().flat_map(|a| a.fv()).cloned().collect();
-        let mut builder = chc::ClauseBuilder::default();
-        let mut pred_sig = chc::PredSig::new();
-        for fv in &fvs {
-            let sort = fv_sort(*fv);
-            builder.add_mapped_var(*fv, sort.clone());
-            pred_sig.push(sort);
-        }
-        for atom in atoms {
-            builder.add_body_mapped(atom);
-        }
-        let pv = self.generate_pred_var(pred_sig);
-        let head = chc::Atom::new(pv.into(), fvs.into_iter().map(chc::Term::var).collect());
-        let clause = builder.head_mapped(head.clone());
-        self.add_clause(clause);
-        head
-    }
 }
 
 impl<'tcx> Analyzer<'tcx> {

src/analyze/annot.rs

@@ -1,10 +1,10 @@
 use rustc_ast::ast::Attribute;
 use rustc_ast::tokenstream::TokenStream;
 use rustc_index::IndexVec;
-use rustc_middle::ty as mir_ty;
 use rustc_span::symbol::{Ident, Symbol};
 
 use crate::annot;
+use crate::chc;
 use crate::rty;
 
 pub fn requires_path() -> [Symbol; 2] {
@@ -31,64 +31,50 @@ pub fn callable_path() -> [Symbol; 2] {
     [Symbol::intern("thrust"), Symbol::intern("callable")]
 }
 
-fn ty_to_term_kind(ty: &mir_ty::Ty<'_>) -> annot::TermKind {
-    match ty.kind() {
-        mir_ty::TyKind::Ref(_, ty, mir_ty::Mutability::Mut) => {
-            annot::TermKind::mut_(ty_to_term_kind(ty))
-        }
-        mir_ty::TyKind::Ref(_, ty, mir_ty::Mutability::Not) => {
-            annot::TermKind::box_(ty_to_term_kind(ty))
-        }
-        mir_ty::TyKind::Adt(def, _) if def.is_box() => annot::TermKind::box_(ty_to_term_kind(ty)),
-        _ => annot::TermKind::other(),
-    }
-}
-
 #[derive(Debug, Clone, Default)]
 pub struct ParamResolver {
-    params: IndexVec<rty::FunctionParamIdx, (Symbol, annot::TermKind)>,
+    params: IndexVec<rty::FunctionParamIdx, (Symbol, chc::Sort)>,
 }
 
 impl annot::Resolver for ParamResolver {
     type Output = rty::FunctionParamIdx;
-    fn resolve(&self, ident: Ident) -> Option<(Self::Output, annot::TermKind)> {
+    fn resolve(&self, ident: Ident) -> Option<(Self::Output, chc::Sort)> {
         self.params
             .iter_enumerated()
             .find(|(_, (name, _))| name == &ident.name)
-            .map(|(idx, (_, kind))| (idx, kind.clone()))
+            .map(|(idx, (_, sort))| (idx, sort.clone()))
     }
 }
 
 impl ParamResolver {
-    pub fn push_param(&mut self, name: Symbol, ty: &mir_ty::Ty<'_>) {
-        self.params.push((name, ty_to_term_kind(ty)));
+    pub fn push_param(&mut self, name: Symbol, sort: chc::Sort) {
+        self.params.push((name, sort));
     }
 }
 
 #[derive(Debug, Clone)]
 pub struct ResultResolver {
     result_symbol: Symbol,
-    result_kind: annot::TermKind,
+    result_sort: chc::Sort,
 }
 
 impl annot::Resolver for ResultResolver {
     type Output = rty::RefinedTypeVar<rty::FunctionParamIdx>;
-    fn resolve(&self, ident: Ident) -> Option<(Self::Output, annot::TermKind)> {
+    fn resolve(&self, ident: Ident) -> Option<(Self::Output, chc::Sort)> {
         if ident.name == self.result_symbol {
-            Some((rty::RefinedTypeVar::Value, self.result_kind.clone()))
+            Some((rty::RefinedTypeVar::Value, self.result_sort.clone()))
         } else {
             None
         }
     }
 }
 
 impl ResultResolver {
-    pub fn new(result_ty: &mir_ty::Ty<'_>) -> Self {
+    pub fn new(result_sort: chc::Sort) -> Self {
         let result_symbol = Symbol::intern("result");
-        let result_kind = ty_to_term_kind(result_ty);
         Self {
             result_symbol,
-            result_kind,
+            result_sort,
         }
     }
 }

src/analyze/basic_block.rs

@@ -101,23 +101,23 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> {
         }
         for ((param_idx, got_ty), expected_ty) in got.params.iter_enumerated().zip(&expected_args) {
             // TODO we can use relate_sub_refined_type here when we implemenented builder-aware relate_*
-            let clause = builder
+            let cs = builder
                 .clone()
                 .with_value_var(&got_ty.ty)
                 .add_body(expected_ty.refinement.clone())
                 .head(got_ty.refinement.clone());
-            clauses.push(clause);
+            clauses.extend(cs);
             builder
                 .with_mapped_value_var(param_idx)
                 .add_body(expected_ty.refinement.clone());
             clauses.extend(builder.relate_sub_type(&expected_ty.ty, &got_ty.ty));
         }
 
-        let clause = builder
+        let cs = builder
             .with_value_var(&got.ret.ty)
             .add_body(got.ret.refinement)
             .head(expected_ret.refinement);
-        clauses.push(clause);
+        clauses.extend(cs);
         clauses.extend(builder.relate_sub_type(&got.ret.ty, &expected_ret.ty));
         clauses
     }
@@ -450,10 +450,8 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> {
                 let ret2 = chc::Term::var(param2_var)
                     .mut_current()
                     .equal_to(chc::Term::var(param1_var).mut_final());
-                let ret_refinement = self
-                    .ctx
-                    .implied_atom(vec![ret1, ret2], |_| param1.ty.to_sort());
-                let ret = rty::RefinedType::new(rty::Type::unit(), ret_refinement.into());
+                let ret_formula = chc::Formula::Atom(ret1).and(chc::Formula::Atom(ret2));
+                let ret = rty::RefinedType::new(rty::Type::unit(), ret_formula.into());
                 rty::FunctionType::new([param1, param2].into_iter().collect(), ret).into()
             }
             Some((def_id, args)) => {
@@ -758,30 +756,37 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> {
     }
 }
 
+/// Turns [`rty::RefinedType<Var>`] into [`rty::RefinedType<T>`].
+///
+/// We sometimes need to replace [`rty::RefinedTypeVar<Var>`] with [`rty::RefinedTypeVar<T>`].
+/// In [`analyze::basic_block`] module, `T` is [`rty::FunctionParamIdx`]. The type we get as
+/// a function result is obtained as [`rty::RefinedTypeVar<Var>`], but we need to express it using
+/// only function parameters for the subtyping. [`UnbindAtoms`] holds the relation between
+/// the function parameters and their representaion under the environment and
+/// let the type in environment be expressed only under the function parameters using existentials.
 #[derive(Debug, Clone)]
 pub struct UnbindAtoms<T> {
     existentials: IndexVec<rty::ExistentialVarIdx, chc::Sort>,
-    atoms: Vec<chc::Atom<rty::RefinedTypeVar<Var>>>,
+    formula: rty::FormulaWithAtoms<rty::RefinedTypeVar<Var>>,
     target_equations: Vec<(rty::RefinedTypeVar<T>, chc::Term<rty::RefinedTypeVar<Var>>)>,
 }
 
 impl<T> Default for UnbindAtoms<T> {
     fn default() -> Self {
         UnbindAtoms {
             existentials: Default::default(),
-            atoms: Default::default(),
+            formula: Default::default(),
             target_equations: Default::default(),
         }
     }
 }
 
 impl<T> UnbindAtoms<T> {
     pub fn push(&mut self, target: rty::RefinedTypeVar<T>, var_ty: PlaceType) {
-        self.atoms.extend(
+        self.formula.push_conj(
             var_ty
-                .conds
-                .into_iter()
-                .map(|a| a.map_var(|v| v.shift_existential(self.existentials.len()).into())),
+                .formula
+                .map_var(|v| v.shift_existential(self.existentials.len()).into()),
         );
         self.target_equations.push((
             target,
@@ -799,14 +804,11 @@ impl<T> UnbindAtoms<T> {
         } = ty;
         let rty::Refinement {
             existentials,
-            atoms,
+            formula,
         } = refinement;
 
-        self.atoms.extend(
-            atoms
-                .into_iter()
-                .map(|a| a.map_var(|v| v.shift_existential(self.existentials.len()))),
-        );
+        self.formula
+            .push_conj(formula.map_var(|v| v.shift_existential(self.existentials.len())));
         self.existentials.extend(existentials);
 
         let mut substs = HashMap::new();
@@ -815,25 +817,29 @@ impl<T> UnbindAtoms<T> {
             substs.insert(v, ev);
         }
 
-        let atoms = self
-            .atoms
-            .into_iter()
-            .map(|a| {
-                a.map_var(|v| match v {
-                    rty::RefinedTypeVar::Value => rty::RefinedTypeVar::Value,
-                    rty::RefinedTypeVar::Free(v) => rty::RefinedTypeVar::Existential(substs[&v]),
-                    rty::RefinedTypeVar::Existential(ev) => rty::RefinedTypeVar::Existential(ev),
+        let mut formula = self.formula.map_var(|v| match v {
+            rty::RefinedTypeVar::Value => rty::RefinedTypeVar::Value,
+            rty::RefinedTypeVar::Free(v) => rty::RefinedTypeVar::Existential(substs[&v]),
+            rty::RefinedTypeVar::Existential(ev) => rty::RefinedTypeVar::Existential(ev),
+        });
+        formula.push_conj(
+            self.target_equations
+                .into_iter()
+                .map(|(t, term)| {
+                    chc::Term::var(t).equal_to(term.map_var(|v| match v {
+                        rty::RefinedTypeVar::Value => rty::RefinedTypeVar::Value,
+                        rty::RefinedTypeVar::Free(v) => {
+                            rty::RefinedTypeVar::Existential(substs[&v])
+                        }
+                        rty::RefinedTypeVar::Existential(ev) => {
+                            rty::RefinedTypeVar::Existential(ev)
+                        }
+                    }))
                 })
-            })
-            .chain(self.target_equations.into_iter().map(|(t, term)| {
-                chc::Term::var(t).equal_to(term.map_var(|v| match v {
-                    rty::RefinedTypeVar::Value => rty::RefinedTypeVar::Value,
-                    rty::RefinedTypeVar::Free(v) => rty::RefinedTypeVar::Existential(substs[&v]),
-                    rty::RefinedTypeVar::Existential(ev) => rty::RefinedTypeVar::Existential(ev),
-                }))
-            }))
-            .collect();
-        let refinement = rty::Refinement::new(self.existentials, atoms);
+                .collect::<Vec<_>>(),
+        );
+
+        let refinement = rty::Refinement::with_formula(self.existentials, formula);
         // TODO: polymorphic datatypes: template needed?
         rty::RefinedType::new(src_ty.assert_closed().vacuous(), refinement)
     }
@@ -872,11 +878,10 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> {
                 }
 
                 let local_ty = self.env.local_type(local);
-                assumption.conds.extend(
+                assumption.formula.push_conj(
                     local_ty
-                        .conds
-                        .into_iter()
-                        .map(|a| a.map_var(|v| v.shift_existential(assumption.existentials.len()))),
+                        .formula
+                        .map_var(|v| v.shift_existential(assumption.existentials.len())),
                 );
                 let term = local_ty
                     .term
@@ -889,16 +894,14 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> {
         for (idx, param) in expected_params.iter_enumerated() {
             let rty::Refinement {
                 existentials,
-                atoms,
+                formula,
             } = param.refinement.clone();
-            assumption.conds.extend(atoms.into_iter().map(|a| {
-                a.subst_var(|v| match v {
-                    rty::RefinedTypeVar::Value => param_terms[&idx].clone(),
-                    rty::RefinedTypeVar::Free(v) => param_terms[&v].clone(),
-                    rty::RefinedTypeVar::Existential(ev) => chc::Term::var(
-                        PlaceTypeVar::Existential(ev + assumption.existentials.len()),
-                    ),
-                })
+            assumption.formula.push_conj(formula.subst_var(|v| match v {
+                rty::RefinedTypeVar::Value => param_terms[&idx].clone(),
+                rty::RefinedTypeVar::Free(v) => param_terms[&v].clone(),
+                rty::RefinedTypeVar::Existential(ev) => chc::Term::var(PlaceTypeVar::Existential(
+                    ev + assumption.existentials.len(),
+                )),
             }));
             assumption.existentials.extend(existentials);
         }