Register enum defs reachable through ADT fields

src/analyze/basic_block.rs

@@ -13,8 +13,8 @@ use crate::analyze;
 use crate::chc;
 use crate::pretty::PrettyDisplayExt as _;
 use crate::refine::{
-    Assumption, BasicBlockType, BasicBlockTypeParamKind, PlaceType, PlaceTypeBuilder, PlaceTypeVar,
-    TempVarIdx, TypeBuilder, Var,
+    Assumption, BasicBlockType, BasicBlockTypeParamKind, EnumDefCollector, PlaceType,
+    PlaceTypeBuilder, PlaceTypeVar, TempVarIdx, TypeBuilder, Var,
 };
 use crate::rty::{
     self, ClauseBuilderExt as _, ClauseScope as _, ShiftExistential as _, Subtyping as _,
@@ -1326,27 +1326,12 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> {
     }
 
     fn register_enum_defs(&mut self) {
+        let mut collector = EnumDefCollector::new(self.type_builder.clone());
         for local_decl in &self.local_decls {
-            use mir_ty::{TypeSuperVisitable as _, TypeVisitable as _};
-            #[derive(Default)]
-            struct EnumCollector {
-                enums: std::collections::HashSet<DefId>,
-            }
-            impl<'tcx> mir_ty::TypeVisitor<mir_ty::TyCtxt<'tcx>> for EnumCollector {
-                fn visit_ty(&mut self, ty: mir_ty::Ty<'tcx>) {
-                    if let mir_ty::TyKind::Adt(adt_def, _) = ty.kind() {
-                        if adt_def.is_enum() {
-                            self.enums.insert(adt_def.did());
-                        }
-                    }
-                    ty.super_visit_with(self);
-                }
-            }
-            let mut visitor = EnumCollector::default();
-            local_decl.ty.visit_with(&mut visitor);
-            for def_id in visitor.enums {
-                self.ctx.get_or_register_enum_def(def_id);
-            }
+            collector.collect(local_decl.ty);
+        }
+        for def_id in collector.into_enums() {
+            self.ctx.get_or_register_enum_def(def_id);
         }
     }
 }

src/chc/format_context.rs

@@ -231,11 +231,25 @@ fn collect_sorts(system: &chc::System) -> BTreeSet<chc::Sort> {
     sorts
 }
 
+fn find_datatype<'a>(
+    datatypes: &'a [chc::Datatype],
+    symbol: &chc::DatatypeSymbol,
+) -> &'a chc::Datatype {
+    datatypes.iter().find(|d| &d.symbol == symbol).unwrap()
+}
+
+fn selector_sorts(datatype: &chc::Datatype) -> impl Iterator<Item = chc::Sort> + '_ {
+    datatype
+        .ctors
+        .iter()
+        .flat_map(|ctor| ctor.selectors.iter().map(|selector| selector.sort.clone()))
+}
+
 fn monomorphize_datatype(
     sort: &chc::DatatypeSort,
     datatypes: &[chc::Datatype],
 ) -> Option<chc::Datatype> {
-    let datatype = datatypes.iter().find(|d| d.symbol == sort.symbol).unwrap();
+    let datatype = find_datatype(datatypes, &sort.symbol);
     if datatype.params == 0 {
         return None;
     }
@@ -269,11 +283,28 @@ fn monomorphize_datatype(
 
 impl FormatContext {
     pub fn from_system(system: &chc::System) -> Self {
-        let mut sorts = collect_sorts(system);
         let mut datatypes = system.datatypes.clone();
-        for sort in sorts.iter().flat_map(|s| s.as_datatype()) {
-            if let Some(mono_datatype) = monomorphize_datatype(sort, &datatypes) {
-                datatypes.push(mono_datatype);
+        let mut sorts = BTreeSet::new();
+        let mut pending: Vec<_> = collect_sorts(system).into_iter().collect();
+        // Declaring a datatype requires the sorts of its selectors to be declared as well,
+        // and those need not occur in the clauses at all: the sort of a field that is only
+        // ever read through a projection is mentioned by the declaration alone.
+        while let Some(sort) = pending.pop() {
+            let mut datatype_sorts = Vec::new();
+            sort.walk(|inner_sort| {
+                if sorts.insert(inner_sort.clone()) {
+                    datatype_sorts.extend(inner_sort.as_datatype().cloned());
+                }
+            });
+            for datatype_sort in datatype_sorts {
+                let datatype = match monomorphize_datatype(&datatype_sort, &datatypes) {
+                    Some(mono_datatype) => {
+                        datatypes.push(mono_datatype.clone());
+                        mono_datatype
+                    }
+                    None => find_datatype(&datatypes, &datatype_sort.symbol).clone(),
+                };
+                pending.extend(selector_sorts(&datatype));
             }
         }
         let int_array_elem_sorts: BTreeSet<_> = sorts

src/refine.rs

@@ -8,7 +8,7 @@
 //! module and remove this one.
 
 mod template;
-pub use template::{TemplateRegistry, TemplateScope, TypeBuilder};
+pub use template::{EnumDefCollector, TemplateRegistry, TemplateScope, TypeBuilder};
 
 mod basic_block;
 pub use basic_block::{BasicBlockType, BasicBlockTypeParamKind};

src/refine/template.rs

@@ -1,4 +1,4 @@
-use std::collections::HashMap;
+use std::collections::{HashMap, HashSet};
 
 use rustc_index::IndexVec;
 use rustc_middle::mir::{Local, Mutability};
@@ -327,6 +327,59 @@ impl<'tcx> TypeBuilder<'tcx> {
     }
 }
 
+/// Collects the enums whose datatype definitions [`TypeBuilder::build`] needs.
+///
+/// A type needs the definition of every enum it mentions, but also of every enum
+/// mentioned by the ADTs it mentions: a struct is elaborated into the tuple of its
+/// fields and an enum into the fields of its variants, so `struct Wrap { o: Option<i32> }`
+/// needs the definition of `Option` even though no `Option` occurs in `Wrap` itself.
+/// Model types are the exception, as they are translated directly without elaborating
+/// their fields.
+pub struct EnumDefCollector<'tcx> {
+    builder: TypeBuilder<'tcx>,
+    elaborated_adts: HashSet<DefId>,
+    enums: HashSet<DefId>,
+}
+
+impl<'tcx> EnumDefCollector<'tcx> {
+    pub fn new(builder: TypeBuilder<'tcx>) -> Self {
+        Self {
+            builder,
+            elaborated_adts: Default::default(),
+            enums: Default::default(),
+        }
+    }
+
+    pub fn collect(&mut self, ty: mir_ty::Ty<'tcx>) {
+        use mir_ty::TypeVisitable as _;
+        ty.visit_with(self);
+    }
+
+    pub fn into_enums(self) -> HashSet<DefId> {
+        self.enums
+    }
+}
+
+impl<'tcx> mir_ty::TypeVisitor<mir_ty::TyCtxt<'tcx>> for EnumDefCollector<'tcx> {
+    fn visit_ty(&mut self, ty: mir_ty::Ty<'tcx>) {
+        use mir_ty::{TypeSuperVisitable as _, TypeVisitable as _};
+
+        let ty = self.builder.resolve_model_ty(ty);
+        if let mir_ty::TyKind::Adt(def, args) = ty.kind() {
+            let is_elaborated = self.builder.model_adt(def, args).is_none();
+            if is_elaborated && self.elaborated_adts.insert(def.did()) {
+                if def.is_enum() {
+                    self.enums.insert(def.did());
+                }
+                for field in def.all_fields() {
+                    field.ty(self.builder.tcx, args).visit_with(self);
+                }
+            }
+        }
+        ty.super_visit_with(self);
+    }
+}
+
 /// Translates [`mir_ty::Ty`] to [`rty::Type`] using templates for refinements.
 ///
 /// [`rty::Template`] is a refinement type in the form of `{ T | P(x1, ..., xn) }` where `P` is a